src/ZF/Cardinal.ML
2000-10-13 paulson renamed fp_Tarski to fp_unfold
2000-09-07 wenzelm tuned ML code (the_context, bind_thms(s));
2000-09-05 paulson new AddIffs (especially Memrel_iff)
2000-08-24 paulson added some xsymbols, and tidied
2000-06-30 paulson removal of batch-style proofs
2000-06-28 paulson fixed some weak elim rules
2000-06-21 paulson new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
2000-02-02 paulson expandshort
2000-01-13 paulson new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
1999-09-07 wenzelm isatool expandshort;
1999-02-03 paulson tidied, with left_inverse & right_inverse as default simprules
1999-01-13 paulson datatype package improvements
1999-01-07 paulson if-then-else syntax for ZF
1998-08-17 paulson Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
1998-08-10 paulson Tidying of AC, especially of AC16_WO4 using a locale
1998-08-06 paulson even more tidying of Goal commands
1998-08-06 paulson Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
1998-08-04 paulson Renamed equals0D to equals0E
1998-07-15 paulson More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson Removal of leading "\!\!..." from most Goal commands
1998-07-13 paulson Huge tidy-up: removal of leading \!\!
1998-07-02 paulson Renamed expand_if to split_if and setloop split_tac to addsplits,
1998-06-22 wenzelm isatool fixgoal;
1997-11-05 paulson Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm isatool fixclasimp;
1997-10-16 wenzelm oops;
1997-10-16 wenzelm transfer thy Ord_nat;
1997-10-10 wenzelm fixed dots;
1997-09-29 paulson Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
1997-04-23 paulson Conversion to use blast_tac
1997-04-04 paulson Another blast_tac call
1997-04-02 paulson Mostly converted to blast_tac
1997-03-18 paulson Stopped giving Introduction rules as Elimination rules
1997-01-08 paulson Removal of sum_cs and eq_cs
1997-01-03 paulson Implicit simpsets and clasets for FOL and ZF
1996-09-26 paulson Ran expandshort; used stac instead of ssubst
1996-06-07 paulson Addition of converse_iff, domain_converse, range_converse as rewrites
1996-05-01 paulson New lemma inspired by KG
1996-03-28 paulson Ran expandshort
1996-03-26 paulson New lemmas for Mutilated Checkerboard
1996-01-30 clasohm expanded tabs
1995-04-14 lcp Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
1995-04-13 lcp Proved lesspoll_succ_iff.
1995-01-11 lcp Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
1994-12-23 lcp Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
1994-12-16 lcp changed useless "qed" calls for lemmas back to uses of "result",
1994-12-15 lcp case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted
1994-12-14 clasohm added bind_thm for theorems defined by "standard ..."
1994-12-08 lcp Card_cardinal_le: new
1994-12-07 clasohm added qed and qed_goal[w]
1994-08-22 lcp ZF/Cardinal: some results moved here from CardinalArith
1994-08-15 lcp ZF/Cardinal/Card_Un: new
1994-07-26 lcp Axiom of choice, cardinality results, etc.
1994-07-12 lcp new cardinal arithmetic developments
1994-06-23 lcp modifications for cardinal arithmetic
1994-06-21 lcp Addition of cardinals and order types, various tidying
less more (0) tip