1999-01-12 ago eliminated global/local names;
1998-12-28 ago new inductive, datatype and primrec packages, etc.
1998-05-27 ago mk_all_imp: no longer creates goals that have beta-redexes
1998-04-10 ago Fixed bug in inductive sections to allow disjunctive premises;
1997-12-03 ago Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
1997-10-17 ago (co) inductive / datatype package adapted to qualified names;
1996-11-28 ago Replaced map...~~ by
1996-11-26 ago Eta-expansion of a function definition, for value polymorphism
1996-05-08 ago moved ap_split to cartprod.ML
1996-01-30 ago expanded tabs
1995-12-22 ago Improving space efficiency of inductive/datatype definitions.
1994-11-24 ago data_domain,Codata_domain: removed replicate; now return one
1994-08-25 ago ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
1994-08-19 ago replaced Lexicon.scan_id by Scanner.scan_id;
1994-08-18 ago ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
1994-08-12 ago installation of new inductive/datatype sections
1994-07-12 ago removed flatten_typ and replaced add_consts by add_consts_i
1994-07-11 ago removed flatten_term and replaced add_axioms by add_axioms_i
1994-07-01 ago replaced extend_theory by new add_* functions;
1994-06-21 ago Addition of cardinals and order types, various tidying
1994-01-18 ago Updated refs to old Sign functions
1993-12-21 ago added []-field to extend_theory: no type abbreviations.
1993-10-22 ago ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
1993-10-15 ago ZF/ind-syntax/refl_thin: new
1993-09-30 ago ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-17 ago Installation of new simplifier for ZF. Deleted all congruence rules not
1993-09-16 ago Initial revision