src/ZF/Zorn.ML
1998-12-28 paulson 1998-12-28 new inductive, datatype and primrec packages, etc.
1998-10-29 paulson 1998-10-29 tidied
1998-10-19 paulson 1998-10-19 fixed some indenting; changed a VERY slow blast_tac to fast_tac
1998-09-10 paulson 1998-09-10 fixed PROOF FAILED
1998-08-14 paulson 1998-08-14 got rid of some goal thy commands
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-08-06 paulson 1998-08-06 Disjointness reasoning by AddEs [equals0E, sym RS equals0E] and consequential changes (and tidying)
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-13 paulson 1998-07-13 Huge tidy-up: removal of leading \!\! addsplits split_tac[split_if] now default nat_succI now included by default
1998-07-02 paulson 1998-07-02 Renamed expand_if to split_if and setloop split_tac to addsplits, as in HOL
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-04-10 paulson 1997-04-10 Changed some fast_tac to blast_tac
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-01-08 paulson 1997-01-08 Removal of sum_cs and eq_cs
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-05-01 lcp 1995-05-01 Simplified proof of Hausdorff_next_exists.
1994-12-19 lcp 1994-12-19 ran expandshort script
1994-12-16 lcp 1994-12-16 changed useless "qed" calls for lemmas back to uses of "result", and/or used "bind_thm" to declare the real results.
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-09-09 lcp 1994-09-09 ZF/Zorn/next_bounded: deleted this proof, which was already in comments
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.