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

Reply via email to