[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] notes on isabelle vs. mizar

I would like to comment on the comparison from the
point of view of an Isabelle user. I use Isabelle/ZF
for my formalized mathematics hobby project.

---+ browsing of Isabelle formalizations sucks
To me the preferred view of Isabelle theories is the
proof document in PDF. It is very readable and easy to
search. It is true that the HTML documents produced my
Isabelle might use the possibilities of web browsing
much better. However, parsing Isar is easy enough that
a motivated person can roll out his/her own rendering
of the theories. I have done so for my project, see
http://formalmath.tiddlyspot.com .

---+ XSymbol vs. ASCII
     XSymbol-ed texts look nice in Emacs and PDF, but
not in ASCII;

I don't quite understand why it would be a desirable
feature for Isabelle theories to look nice in an ASCII
editor. ASCII editors are not good tools for
presenting or authoring mathematics, formalized or
not. ProofGeneral is a decent authoring tool for
Isabelle and PDF proof documents are good for
browsing. 
One of the features of Isabelle that I like a lot is
that it supports a (potentially) unlimited number of
symbols.  This allows to create renderings of
formalized text that are very close to traditional
mathematical notation. It is just not possible with
the set of symbols limited to ASCII.

http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)


      ____________________________________________________________________________________
Looking for last minute shopping deals?  
Find them fast with Yahoo! Search.  http://tools.search.yahoo.com/newsearch/category.php?category=shopping