src/ZF/ex/misc.ML
1997-12-24 ago New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-28 ago New example
1997-11-05 ago Ran expandshort, especially to introduce Safe_tac
1997-11-04 ago isatool fixclasimp;
1997-11-03 ago isatool fixclasimp;
1997-04-21 ago Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
1997-01-09 ago Removal of needless "addIs [equality]", etc.
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1996-06-03 ago Shortened a proof
1996-04-04 ago updated comments
1996-01-30 ago expanded tabs
1995-05-04 ago Changed some definitions and proofs to use pattern-matching.
1994-12-14 ago added bind_thm for theorems defined by "standard ..."
1994-11-24 ago moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
1994-11-03 ago ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
1994-06-21 ago Various updates and tidying
1993-10-07 ago used ~: for "not in"
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/ex. The hom_ss example in misc.ML is
1993-09-16 ago Initial revision