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;