wenzelm [Sat, 09 Dec 2006 18:05:42 +0100] rev 21723
renamed reserved to reserved_names;
added reserved: Name.context;
wenzelm [Sat, 09 Dec 2006 18:05:41 +0100] rev 21722
tuned Consts signature;
wenzelm [Sat, 09 Dec 2006 18:05:40 +0100] rev 21721
abbrevs: print original rhs;
wenzelm [Sat, 09 Dec 2006 18:05:39 +0100] rev 21720
abbreviate: always authentic, force expansion of internal abbreviations;
tuned signature;
tuned;
wenzelm [Sat, 09 Dec 2006 18:05:38 +0100] rev 21719
ML_Syntax.reserved(_names);
wenzelm [Sat, 09 Dec 2006 18:05:37 +0100] rev 21718
TermSyntax.abbrev;
wenzelm [Sat, 09 Dec 2006 18:05:36 +0100] rev 21717
added antiquotation abbrev;
wenzelm [Sat, 09 Dec 2006 18:05:34 +0100] rev 21716
added print_abbrevs;
wenzelm [Fri, 08 Dec 2006 23:25:54 +0100] rev 21715
tuned use_text;
eval command line: skip over -q option;
wenzelm [Fri, 08 Dec 2006 23:25:53 +0100] rev 21714
added 'help' command (same of 'print_commands');