Re: Math Notations, Computer Languages, and the “Form” in Formalism
skokodyn at yahoo.com
Sat Sep 5 16:41:17 CEST 2009
> Theorem provers
> such as OCaml (HOL, Coq), Mizar does math formalism as a foundation,
> also function as a generic computer language, but lacks abilities as a
> computer algebra system or math notation representation.
Isabelle's presentation layer is well integrated with LaTeX and you
can use math notation in (presentation of) proofs.
More information about the Python-list