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];
1995-01-18 clasohm 1995-01-18 added optional precedence for body of binder; removed call to infer_types from read_xrules
1994-12-09 wenzelm 1994-12-09 minor internal changes;
1994-12-07 clasohm 1994-12-07 moved first call of store_theory from thy_read.ML to created .thy.ML file
1994-11-14 wenzelm 1994-11-14 exported 'cat';
1994-10-25 wenzelm 1994-10-25 strip_quotes now exported;
1994-10-12 wenzelm 1994-10-12 type_args, opt_witness now exported; added AxClass.;
1994-09-07 clasohm 1994-09-07 renamed temporary variable 'base' to 'thy' in mk_structure
1994-09-06 clasohm 1994-09-06 renamed base_on into mk_base and moved it to the beginning of the generated .thy.ML file to make sure that all base theories are present when ML executes the rest of this file
1994-08-22 lcp 1994-08-22 Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens, brackets, ..., mk_triple
1994-08-19 wenzelm 1994-08-19 renamed 'defns' to 'defs'; removed 'sigclass'; replaced parents by enclose; exported parens, brackets, mk_list, mk_big_list, mk_pair, mk_triple; various minor internal changes;
1994-07-15 clasohm 1994-07-15 added check for concistency of filename and theory name; made loaded_thys a symtab instead of an association list; added store_thm, qed, get_thm, get_thms
1994-07-06 wenzelm 1994-07-06 exported opt_infix, opt_mixfix parsers; removed 'subclass' section (now handled by 'instance'); improved make_syntax: section names now added automatically to keywords;
1994-06-16 wenzelm 1994-06-16 added 'subclass' section; minor internal cleanups;
1994-06-01 wenzelm 1994-06-01 added signature constraint; replaced 'also' by '|>'; added 'sigclass' section; removed pure_syntax;
1994-05-19 wenzelm 1994-05-19 (replaces Thy/parse.ML and Thy/syntax.ML) much simpler because of new theory extension functions; theory is now built up from an arbitrary list of definable 'sections'; new axclass and instance sections;