src/ZF/simpdata.ML
1995-01-12 ago Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
1994-12-08 ago test_assume_tac: now tries eq_assume_tac on exceptional cases
1994-08-16 ago ZF/pair.ML: moved some definitions here from simpdata.ML
1994-08-12 ago installation of new inductive/datatype sections
1994-07-26 ago Axiom of choice, cardinality results, etc.
1994-07-12 ago new cardinal arithmetic developments
1994-06-21 ago Addition of cardinals and order types, various tidying
1994-03-17 ago Improved layout for inductive defs
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