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-29 ago ZF/intr_elim/intro_tacsf: now uses SigmaI as a default intro rule and
1994-07-15 ago added thy_name to Datatype_Fun's parameter
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-10-05 ago ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
1993-09-30 ago ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-16 ago Initial revision