On Sat, 21 Apr 2012, Bill Richter wrote:
Mizar has a particularly annoying feature of not allowing TABs or the
symbols for implies etc which Isabelle/Isar (which I never built or
understood) uses. So I wrote some emacs code .mizar-isar.el which gets
around this. Now I write up my Mizar code in Isar fashion, using the
forbidden symbols ⇒ ¬ ∨ ∧ ≡ ∀ ∃ ⇔ and not worrying abo
I was occasionally considering to disallow TABs formally in Isabelle/Isar
as well -- they just introduce too many problems for very little benefit.
To start using Isabelle/Isar you should not "build" it, just take one of
the platform-specific distribution bundles from its download page and run
it.
The different prover platforms all have their own cultural background.
And for starting a serious project you should try to figure out which
culture accomodates your own most closely.
Makarius
------------------------------------------------------------------------------
For Developers, A Lot Can Happen In A Second.
Boundary is the first to Know...and Tell You.
Monitor Your Applications in Ultra-Fine Resolution. Try it FREE!
http://p.sf.net/sfu/Boundary-d2dvs2
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info