[isabelle-dev] Deprecating legacy ASCII symbols?
makarius at sketis.net
Tue Aug 4 21:38:34 CEST 2015
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
Including the results from the discussion on this thread, the plan is now
* 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
More information about the isabelle-dev