ottversion
Ott is a tool for writing definitions of programming languages and calculi
It 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 LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by targetsystem 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  Hannes Mehnert <hannes@mehnert.org> 
Dependencies 

Source [http]  http://www.cl.cam.ac.uk/~pes20/ott/ott_distro_0.21.2.tar.gz md5=e9a5dae61b0aa5c33c3445e8e8a92b6a 
Statistics  Installed 2 times last month. 
Edit  https://github.com/ocaml/opamrepository/tree/master/packages/ott/ott.0.21.2/opam 
No package is dependent