ottversion
A tool for writing definitions of programming languages and calculi
Ott takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates output:
 a LaTeX source file that defines commands to build a typeset version of the definition;
 a Coq version of the definition;
 a HOL version of the definition;
 an Isabelle/HOL version of the definition;
 a Lem version of the definition;
 an OCaml version of the syntax of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by typeset terms.
Authors  Peter Sewell, Francesco Zappa Nardelli and Scott Owens 

Licenses  BSD3Clause and LGPL2.1only 
Published  
Homepage  http://www.cl.cam.ac.uk/~pes20/ott/ 
Issue Tracker  https://github.com/ottlang/ott/issues 
Maintainer  Thibaut PĂ©rami <Thibaut.Perami@cl.cam.ac.uk> 
Dependencies 

Source [http]  https://github.com/ottlang/ott/archive/0.32.tar.gz md5=f36d94978be65d7837fe4a1c24672d2e sha512=f38e12c079426c5a460a9ab24e58f098410ceb5ae0284c1719c50f6d7cd88f6b9c4da6beb5425c03f2dc056c7a9cb597f9bf2983abb525e3c003e45858496ad3 
Edit  https://github.com/ocaml/opamrepository/tree/master/packages/ott/ott.0.32/opam 