Lightweight Executable Mathematics for large-scale portable semantics

Lem is a tool for lightweight executable mathematics, for writing, managing, and publishing large-scale portable semantic definitions, with export to LaTeX, executable code (currently OCaml) and interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL).

It is also intended as an intermediate language for generating definitions from domain-specific tools, and for porting definitions between interactive theorem proving systems.

Lem is under active development and has been used in several applications, some of which can be found in the examples directory. It is made available under the BSD 3-clause license, with the exception of a few files derived from OCaml, which are under the GNU Library GPL.