Re: Math Notations, Computer Languages, and the “Form” in Formalism

[slawekk]

> 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.

Slawekk