etc/symbols
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.