src/Pure/Isar/spec_parse.ML
2009-10-28 wenzelm 2009-10-28 provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
2009-03-26 wenzelm 2009-03-26 locale_expression: mandatory as parameter; misc tuning and simplifications of parsers;
2009-03-25 wenzelm 2009-03-25 tuned;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-12 wenzelm 2009-03-12 removed old named_spec, spec_name, spec_opt_name; clarified spec vs. specs; added alt_specs, where_alt_specs -- try to be robust against malformed input;
2009-01-21 wenzelm 2009-01-21 tuned whitespace;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2009-01-02 wenzelm 2009-01-02 added type 'a parser, simplified signature;
2008-12-14 ballarin 2008-12-14 Strict prefixes in locales expressions.
2008-12-10 ballarin 2008-12-10 Enable keyword 'structure' in for clause of locale expression.
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-06 ballarin 2008-11-06 Minor cleanup.
2008-10-30 ballarin 2008-10-30 Dropped context element 'includes'.
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations; moved thm_sel to attrib.ML;
2008-06-28 wenzelm 2008-06-28 tuned;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2007-10-19 ballarin 2007-10-19 Interpretation equations may have name and/or attribute.
2007-10-06 wenzelm 2007-10-06 added class_expr; tuned;
2007-07-27 wenzelm 2007-07-27 attribs: not cut (!!!);
2007-07-27 wenzelm 2007-07-27 xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
2007-07-23 ballarin 2007-07-23 interpretation: equations are propositions not pairs of terms;
2007-04-13 ballarin 2007-04-13 Experimental interpretation code for definitions.
2007-01-19 wenzelm 2007-01-19 Parsers for complex specifications (material from outer_parse.ML);