Re: [mizar] notes on isabelle vs. mizar

[Makarius <makarius@sketis.net>]

On Thu, 27 Mar 2008, Bartek wrote:

> Josef Urban wrote:
> > > ASCII editors are not good tools for
> > > presenting or authoring mathematics, formalized or
> > > not.
> >
> > I would agree with presenting, authoring is a different matter. The Mizar
> > team even went from nonASCII-allowed to ASCII-only couple of years ago for
> > purely practical reasons, and people got used very quickly to "in" instead
> > of the \epsilon character. 
> Josef, Slawomir is right. For authoring mathematics: still a blackboard or
> sheet of paper rule:)))

I agree.  A whiteboard is also quite nice -- only the classical one 
*without* printout facilities.


> Of course, ASCII editors for writing less-formal (or as you prefer 
> non-formal) mathematics in LaTeX are the most popular. This is the one 
> and only way to do this since this is what journals accept. Even if some 
> crazy guy uses tools like ScientificWorkPlace, he ends up correcting the 
> source using notepad in order to meet the journal requirements (I really 
> know some of these guys).

The Isabelle sources are essentially a stylized version of formal LaTeX.  
As a side effect of formal processing you get real LaTeX.  By providing an 
appropriate header (with document class setup, macro definitions) you get 
a publishable document.  We have routinely used this system for several 
years to produce articles for conferences /journals, and theses / books, 
as well as presentations (e.g. using foiltex).


	Makarius