src/ZF/CardinalArith.ML
2000-09-07 wenzelm tuned ML code (the_context, bind_thms(s));
2000-09-05 paulson new AddIffs (especially Memrel_iff)
2000-08-01 paulson natify, a coercion to reduce the number of type constraints in arithmetic
2000-06-28 paulson tidying and unbatchifying
2000-03-22 paulson tidied using new "inst" rule
2000-02-07 paulson tidied some proofs
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-27 paulson new typechecking solver for the simplifier
1999-01-07 paulson ZF: the natural numbers as a datatype
1999-01-07 paulson if-then-else syntax for ZF
1998-09-22 paulson tidying
1998-09-15 paulson tidied
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-07-15 paulson More tidying and removal of "\!\!... from 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-12-24 paulson New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-27 paulson Tidying, mostly indentation
1997-11-05 paulson Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm isatool fixclasimp;
1997-10-16 wenzelm transfer CardinalArith.thy nat_into_Ord;
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-09 paulson Using Blast_tac
1997-01-08 paulson Removal of sum_cs and eq_cs
1997-01-03 paulson Implicit simpsets and clasets for FOL and ZF
1996-03-28 paulson New theorem Finite_imp_succ_cardinal_Diff
1996-03-26 paulson New lemmas for Mutilated Checkerboard
1996-01-30 clasohm expanded tabs
1995-05-03 lcp Changed some definitions and proofs to use pattern-matching.
1995-04-28 lcp Modified proofs for new claset primitives. The problem is that they enforce
1995-03-31 lcp Tried the new addss in a proof.
1995-01-20 lcp Replaced ordermap_z_lepoll by ordermap_z_lt, which is
1995-01-11 lcp Now proof of Ord_jump_cardinal uses
1994-12-23 lcp Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit
1994-12-16 lcp Limit_csucc: moved to InfDatatype and proved explicitly in
1994-12-14 clasohm added bind_thm for theorems defined by "standard ..."
1994-12-08 lcp sum_lepoll_self, cadd_le_self, prod_lepoll_self,
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/CardinalArith/InfCard_Un: new
1994-08-12 lcp for infinite datatypes with arbitrary index sets
1994-08-12 lcp installation of new inductive/datatype sections
1994-07-27 lcp Addition of infinite branching datatypes
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
less more (0) tip