2011-08-17 ago modernized signature of Term.absfree/absdummy;
2010-12-20 ago proper identifiers for consts and types;
2010-09-12 ago eliminated aliases of Type.constraint;
2010-08-18 ago deglobalization
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-02-15 ago discontinued unnamed infix syntax;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-29 ago standardized filter/filter_out;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-17 ago explicitly qualify Drule.standard;
2009-10-15 ago replaced String.concat by implode;
2009-09-29 ago modernized Balanced_Tree;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-03-07 ago more uniform handling of binding in packages;
2008-12-04 ago cleaned up binding module and related code
2008-06-18 ago eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-06-16 ago pervasive RuleInsts;
2008-06-16 ago RuleInsts.read_instantiate;
2008-06-11 ago Drule.read_instantiate;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-03-01 ago misc cleanup of embedded ML code;
2008-02-11 ago removed unnecessary theory qualifiers;
2008-02-11 ago Made theory names in ZF disjoint from HOL theory names to allow loading both developments
2007-10-07 ago modernized specifications;
2007-10-03 ago avoid unnamed infixes;
2007-06-19 ago BalancedTree;
2007-05-31 ago removed obsolete IFOL.thy/FOL.thy values;
2007-04-03 ago removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2006-11-26 ago converted legacy ML scripts;
2005-11-16 ago Term.betapply;
2005-10-25 ago traceIt: plain term;
2005-07-15 ago tuned fold on terms and lists;
2005-03-03 ago Move towards standard functions.
2002-05-15 ago better error messages for datatypes not declared Const
2001-11-19 ago tuned;
2000-05-05 ago use Sign.simple_read_term;
1999-10-04 ago tryres, gen_make_elim moved here;
1999-01-13 ago datatype package improvements
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.