src/Pure/Isar/outer_parse.ML
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2002-02-26 wenzelm 2002-02-26 renamed "uses" to "includes";
2002-02-25 wenzelm 2002-02-25 export locale_target, locale_keyword;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2001-11-22 wenzelm 2001-11-22 improved locale expression syntax;
2001-11-22 wenzelm 2001-11-22 added uname; syntax for locale expressions (presently unused);
2001-11-21 wenzelm 2001-11-21 locale expressions;
2001-11-06 wenzelm 2001-11-06 locale_element/uses: string;
2001-11-06 wenzelm 2001-11-06 group locale_element;
2001-11-05 wenzelm 2001-11-05 locale_element: optional typ;
2001-11-04 wenzelm 2001-11-04 added locale_element;
2001-10-16 wenzelm 2001-10-16 parser for underscore (actually a symbolic identifier!);
2001-10-02 wenzelm 2001-10-02 support non-oriented infix;
2000-06-27 wenzelm 2000-06-27 OuterLex.name_of: include val;
2000-06-25 wenzelm 2000-06-25 added semicolon; added arguments; tuned;
2000-06-04 wenzelm 2000-06-04 opt_mixfix', opt_infix';
2000-05-21 wenzelm 2000-05-21 adapted to inner syntax of sorts;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-01 wenzelm 2000-04-01 tuned mixfix syntax;
2000-03-26 wenzelm 2000-03-26 made SML/NJ happy;
2000-03-26 wenzelm 2000-03-26 !!!! = cut "Corrupted outer syntax in presentation";
2000-03-06 wenzelm 2000-03-06 argument: include verbatim;
2000-02-13 wenzelm 2000-02-13 tuned attrib;
2000-01-26 wenzelm 2000-01-26 'name' etc. include 'number'; attrib: include keyword_sid as name;
1999-12-22 wenzelm 1999-12-22 marg_comment: repeat;
1999-10-26 wenzelm 1999-10-26 added opt_unit (from isar_syn.ML);
1999-09-04 wenzelm 1999-09-04 removed text vars;
1999-09-01 wenzelm 1999-09-01 any_props: improved error; removed "*" method combinator;
1999-08-25 wenzelm 1999-08-25 fixed arity;
1999-08-03 wenzelm 1999-08-03 improved interest;
1999-07-16 wenzelm 1999-07-16 separate command tokens;
1999-07-12 wenzelm 1999-07-12 term/prop: include number; method args: exlude method meta chars;
1999-07-09 wenzelm 1999-07-09 added termp;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns;
1999-06-30 wenzelm 1999-06-30 added sync;
1999-05-25 wenzelm 1999-05-25 renamed Comment.empty to Comment.none;
1999-04-30 wenzelm 1999-04-30 method = meth3 (again);
1999-04-30 wenzelm 1999-04-30 comment, interest;
1999-04-27 wenzelm 1999-04-27 opt_thm_name: name optional;
1999-04-14 wenzelm 1999-04-14 triple_swap;
1999-03-17 wenzelm 1999-03-17 fixed thm_name again;
1999-03-17 wenzelm 1999-03-17 added simple_arity, spec_name, spec_opt_name; tuned thm_name; xthms1: no 'and' separators;
1999-03-11 wenzelm 1999-03-11 tuned opt_mixfix failure;
1998-12-03 wenzelm 1998-12-03 and_list;
1998-12-01 wenzelm 1998-12-01 enum: !!! after seperator;
1998-11-25 wenzelm 1998-11-25 comment parser;
1998-11-19 wenzelm 1998-11-19 fixed method syntax;
1998-11-17 wenzelm 1998-11-17 generalized (opt_)thm_name; xthm, xthms1;
1998-11-16 wenzelm 1998-11-16 removed args, args1, thm_xname; fixed nat: Symbol.explode; name / xname: include sym_ident; keyword_symid: include ident; tuned atom_arg; support nested args;
1998-11-09 wenzelm 1998-11-09 Generic parsers for Isabelle/Isar outer syntax.