etc/symbols
2010-05-31 wenzelm 2010-05-31 tuned abbrevs for long arrows, according to usual ASCII syntax;
2009-10-29 wenzelm 2009-10-29 removed slightly exotic symbol abbreviations for now -- achieves a coherent (unique) mapping; (NB: in principle symbol abbreviations could well be ambigous);
2009-10-23 tbourke 2009-10-23 Fix a duplicate abbreviation || in etc/symbols.
2009-06-26 wenzelm 2009-06-26 tuned abbrevs;
2009-06-23 wenzelm 2009-06-23 fixed abbrev !! for \<And>;
2008-12-20 wenzelm 2008-12-20 removed Ids;
2008-08-24 wenzelm 2008-08-24 activated \<A>, \<a>, \<AA>, \<aa>; disabled \<RR>, \<II> which overlap with codepoints for \<Re>, \<Im>, remapped to unofficial place within Isabelle font;
2008-08-16 wenzelm 2008-08-16 tuned abbrevs;
2008-08-15 wenzelm 2008-08-15 added some abbrevs; \<euro>: from default font;
2008-08-15 wenzelm 2008-08-15 removed redundant "symbol" property; added "font" propery; disabled alternative letters (\<A> etc.) for now;
2008-08-15 wenzelm 2008-08-15 Default interpretation of some Isabelle symbols.