This thread is still pending.
At the Isabelle tutorial at CADE-25, we've had again the situation that
new users got very confused by the odd ASCII syntax in basic theories of
Main Isabelle/HOL.
Including the results from the discussion on this thread, the plan is now
as follows:
* print mode "xsymbols" looses its special status eventually, and
Isabelle symbols are used by default
* print mode "ASCII" retains some important old-style ASCII syntax, e.g.
basic things like !! ==> ALL EX --> & | :
* strange and/or rarely used ASCII notation is eliminated -- depending
on actual use in the visible universe of Isabelle + AFP applications
* \<Colon> is eliminated and :: used exclusively
This is quite conservative. It mainly means that theory sources are
cleaned up a bit, and the default print mode setup is simplified.
Questions about particular syntax may be discussed on this thread
eventually.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
