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.24.tar.gz md5=6512a2b737cb8408348306378fc46553 
Statistics  Installed 2 times last month. 
Edit  https://github.com/ocaml/opamrepository/tree/master/packages/ott/ott.0.24/opam 
No package is dependent