src/ZF/ind_syntax.ML
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 ListPair.map
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