src/Pure/Thy/thy_parse.ML
1999-03-11 wenzelm 1999-03-11 tuned space;
1999-03-09 wenzelm 1999-03-09 IsarThy.begin/end_theory;
1999-02-03 wenzelm 1999-02-03 get_lexicon; parse_thy: eliminated name, get exploded text; simplified header handling;
1999-01-12 wenzelm 1999-01-12 eliminated Attribute structure;
1998-12-28 paulson 1998-12-28 more efficient strip_quotes using "substring"
1998-12-11 paulson 1998-12-11 the + facility for locales, by Florian
1998-12-04 paulson 1998-12-04 locales: assumes and defines may be empty
1998-11-17 wenzelm 1998-11-17 Theory.apply replaced by Library.apply;
1998-10-20 wenzelm 1998-10-20 Syntax.max_pri;
1998-08-04 wenzelm 1998-08-04 added 'locale' section;
1998-06-20 wenzelm 1998-06-20 export mk_triple1/2;
1998-05-25 wenzelm 1998-05-25 tuned local, global; tuned begin and end theory;
1998-05-20 wenzelm 1998-05-20 tuned keywords;
1998-04-29 wenzelm 1998-04-29 replaced thy_setup by 'setup' section; adapted to new PureThy.add_axioms / PureThy.add_defs; added 'nonterminals' section;
1998-04-04 wenzelm 1998-04-04 replaced thy_data by thy_setup;
1998-03-09 wenzelm 1998-03-09 tuned;
1997-12-29 wenzelm 1997-12-29 removed distinct_fst_string;
1997-12-04 wenzelm 1997-12-04 moved global_names ref to Pure/ROOT.ML;
1997-11-03 wenzelm 1997-11-03 added MLtext section;
1997-11-03 wenzelm 1997-11-03 tuned: distinct_fst_string;
1997-11-03 wenzelm 1997-11-03 export const_decls parser;
1997-10-31 wenzelm 1997-10-31 dup sections: warning instead of error;
1997-10-30 wenzelm 1997-10-30 added thy_data;
1997-10-28 wenzelm 1997-10-28 PureThy.add_store_defs, PureThy.add_store_axioms;
1997-10-27 wenzelm 1997-10-27 flipped global_names default;
1997-10-23 wenzelm 1997-10-23 improved typ parser, exported;
1997-10-20 wenzelm 1997-10-20 make SML/NJ happy;
1997-10-20 wenzelm 1997-10-20 local section; improved global, local;
1997-10-17 paulson 1997-10-17 Eta-expanded a function decl to make sml/nj happy
1997-10-16 wenzelm 1997-10-16 removed begin; added global section; added global_names flag (tmp), default true;
1997-10-15 wenzelm 1997-10-15 eliminated aliasing merge: now always extends;
1997-10-09 wenzelm 1997-10-09 improved oracle: name; optional begin after thy header, with warning;
1997-10-06 wenzelm 1997-10-06 fixed 'begin';
1997-10-06 wenzelm 1997-10-06 optional begin keyword;
1997-10-06 wenzelm 1997-10-06 added 'path' section; root path at end;
1997-10-01 wenzelm 1997-10-01 fully qualified name: Theory.set_oracle;
1997-10-01 wenzelm 1997-10-01 fully qualified names: Theory.add_XXX;
1997-07-18 wenzelm 1997-07-18 renamed |-> <-| <-> to Parse/PrintRule;
1997-05-06 wenzelm 1997-05-06 removed MLtrans, MLtext;
1997-02-28 wenzelm 1997-02-28 added token_translation interface;
1996-12-13 wenzelm 1996-12-13 added typed print translations;
1996-12-10 wenzelm 1996-12-10 syntax section: added 'output' mode option;
1996-11-27 wenzelm 1996-11-27 use_thy now automatically opens theory structures;
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-18 wenzelm 1996-11-18 mixfix: added syntax for Infirl/rName; syntax section: added option printer table name;
1996-07-11 paulson 1996-07-11 Oracles can now be strings instead of identifiers
1996-06-18 paulson 1996-06-18 Translation infixes <->, etc., no longer available at top-level
1996-04-30 clasohm 1996-04-30 changed ident_no_colon so that it forbids postfix "=", too
1996-03-06 clasohm 1996-03-06 added constdefs
1996-03-05 paulson 1996-03-05 Addition of oracles
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1995-12-01 clasohm 1995-12-01 added const_type to type_decl
1995-12-01 clasohm 1995-12-01 simplified parser for constType
1995-11-29 clasohm 1995-11-29 added type class to simple_type
1995-11-07 clasohm 1995-11-07 types in consts section of .thy files can now be specified without quotes
1995-09-06 clasohm 1995-09-06 removed list2 and enum2
1995-09-06 clasohm 1995-09-06 added enum2 and list2
1995-08-21 wenzelm 1995-08-21 minor fix to make less noise with SML/NJ;
1995-04-11 nipkow 1995-04-11 (binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).
1995-01-27 wenzelm 1995-01-27 binder: optional body pri now [bracketted];