> 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 -- http://mail.python.org/mailman/listinfo/python-list
