src/ZF/Cardinal.ML
2000-06-30 paulson 2000-06-30 removal of batch-style proofs
2000-06-28 paulson 2000-06-28 fixed some weak elim rules
2000-06-21 paulson 2000-06-21 new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
2000-02-02 paulson 2000-02-02 expandshort
2000-01-13 paulson 2000-01-13 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed from directory AC
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-02-03 paulson 1999-02-03 tidied, with left_inverse & right_inverse as default simprules
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-07 paulson 1999-01-07 if-then-else syntax for ZF
1998-08-17 paulson 1998-08-17 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy contains fewer theorems than before
1998-08-10 paulson 1998-08-10 Tidying of AC, especially of AC16_WO4 using a locale
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-08-04 paulson 1998-08-04 Renamed equals0D to equals0E
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most 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-10-16 wenzelm 1997-10-16 oops;
1997-10-16 wenzelm 1997-10-16 transfer thy Ord_nat;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-29 paulson 1997-09-29 Much tidying including step_tac -> clarify_tac or safe_tac; sometimes used qed_spec_mp
1997-04-23 paulson 1997-04-23 Conversion to use blast_tac
1997-04-04 paulson 1997-04-04 Another blast_tac call
1997-04-02 paulson 1997-04-02 Mostly converted to blast_tac
1997-03-18 paulson 1997-03-18 Stopped giving Introduction rules as Elimination rules
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-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-06-07 paulson 1996-06-07 Addition of converse_iff, domain_converse, range_converse as rewrites
1996-05-01 paulson 1996-05-01 New lemma inspired by KG
1996-03-28 paulson 1996-03-28 Ran expandshort
1996-03-26 paulson 1996-03-26 New lemmas for Mutilated Checkerboard
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-04-14 lcp 1995-04-14 Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll to Diff_sing_lepoll, lepoll_Diff_sing and Diff_sing_eqpoll for consistency. Strengthened lepoll_Diff_sing. (Thanks to KG)
1995-04-13 lcp 1995-04-13 Proved lesspoll_succ_iff.
1995-01-11 lcp 1995-01-11 Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong uses lemma sum_bij; proof of prod_eqpoll_cong uses lemma prod_bij.
1994-12-23 lcp 1994-12-23 Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD, succ_eqpoll_succD, cons_lepoll_cons_iff, cons_eqpoll_cons_iff. Deleted inj_succ_succD. Streamlined proof of nat_lepoll_imp_le_lemma. Added Krzysztof's theorems diff_sing_lepoll, lepoll_diff_sing, diff_sing_eqpoll, lepoll_1_is_sing, inj_not_surj_succ, lesspoll_trans, lesspoll_lepoll_lesspoll, lepoll_lesspoll_lesspoll, lepoll_imp_lesspoll_succ, lesspoll_succ_imp_lepoll, lepoll_succ_disj, lepoll_nat_imp_Finite, lepoll_Finite, Finite_imp_cons_Finite, Finite_imp_succ_Finite, nat_le_infinite_Ord, nat_wf_on_converse_Memrel, nat_well_ord_converse_Memrel, well_ord_converse, ordertype_eq_n, Finite_well_ord_converse
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-15 lcp 1994-12-15 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted own bij_inverse_ss and replaces uses by case_ss
1994-12-14 clasohm 1994-12-14 added bind_thm for theorems defined by "standard ..."
1994-12-08 lcp 1994-12-08 Card_cardinal_le: new
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-08-22 lcp 1994-08-22 ZF/Cardinal: some results moved here from CardinalArith ZF/CardinalArith/nat_succ_lepoll: removed obsolete proof ZF/CardinalArith/nat_cons_eqpoll: new
1994-08-15 lcp 1994-08-15 ZF/Cardinal/Card_Un: new
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.
1994-07-12 lcp 1994-07-12 new cardinal arithmetic developments
1994-06-23 lcp 1994-06-23 modifications for cardinal arithmetic
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying