src/ZF/pair.ML
1997-12-24 ago New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-03 ago isatool fixclasimp;
1997-10-10 ago fixed dots;
1997-04-02 ago Converted to call blast_tac.
1997-01-08 ago Removal of sum_cs and eq_cs
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1996-01-30 ago expanded tabs
1995-05-03 ago Modified proofs for (q)split, fst, snd for new
1995-01-12 ago prove_fun now includes equalityI. Added the rewrite rules
1994-12-23 ago Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
1994-12-14 ago added bind_thm for theorems defined by "standard ..."
1994-12-07 ago added qed and qed_goal[w]
1994-08-16 ago ZF/pair.ML: moved some definitions here from simpdata.ML
1994-06-23 ago modifications for cardinal arithmetic
1994-06-21 ago Addition of cardinals and order types, various tidying
1993-09-17 ago Installation of new simplifier for ZF. Deleted all congruence rules not
1993-09-16 ago Initial revision