[isabelle-dev] Deprecating legacy ASCII symbols?

[Makarius]

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