I'll present what tmEgg does differently than the usual Coq (and other proof assistants) user interfaces, how this is important in a document-oriented setting, what tmEgg does differently than the TeXmacs-CAS integration plugins and how this is important in the context of a proof assistant. ) instead of merely character strings.Д¬oq is a LCF-style (procedural) proof assistant that is a proof assistant where one progresses in the proof by telling it what to do rather than what the intermediary steps in the proof are. TeXmacs allows the WYSIWYG authoring of scientific documents (at a level of abstraction similar to LaTeX) and is used as a user interface to several computer algebra systems, including the use of true mathematical notations (fractions, sigmas, integration symbols, indices.

Re: Texmacs-dev paste verbatim interprets in red Miguel de Benito Delgado Texmacs-dev cleanup in color managment FranГ§ois Poulain. This software, tmEgg, turns TeXmacs into a new user interface to Coq. Re: Texmacs-dev building texmacs FranГ§ois Poulain Texmacs-dev paste verbatim interprets in red Sam Liddicott. texmacs symbols

I will discuss the integration of the authoring of a mathematical document and the formalisation of the mathematics contained in that document in a procedural proof assistant through the example of thecurrently in development integration between the Coq proof management system and the TeXmacs scientific editor. 1 shows how the above example definition and notation appear in a TEXMACS document. Lionel Elie Mamane (Radboud University Nijmegen)

TmEgg: Documented-oriented interaction with the Coq theorem prover

Texmacs symbols