Re: [mizar] notes on isabelle vs. mizar

[Bartek <bartek@math.uwb.edu.pl>]

Hi guys,

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:)))

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).
> I think that this might change over time, e.g. with good Unicode tools 
> (in this sense XSymbol is still ASCII, which is good).
But then someone has to create a special keyboard for writing maths;) 
These things would be great. So far auctex mode in emacs has to do the 
trick for me.

Bartek