src/HOL/Nat.ML
1998-07-24 berghofe 1998-07-24 Declaration of type 'nat' as a datatype (this allows usage of exhaust_tac and induct_tac on type 'nat'). Moved some proofs using natE from NatDef.ML to Nat.ML.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-04-23 paulson 1997-04-23 Ran expandshort
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1996-12-18 oheimb 1996-12-18 added nat_induct2
1996-11-28 nipkow 1996-11-28 Missing case in instantiation of Transitivity prover (negate(None)=None)
1996-11-07 paulson 1996-11-07 Adding lessI to default claset
1996-10-21 nipkow 1996-10-21 Added trans_tac (see Provers/nat_transitive.ML)
1996-10-16 nipkow 1996-10-16 Defined pred using nat_case rather than nat_rec. Added expand_nat_case
1996-10-10 paulson 1996-10-10 Removed Fast_tac made redundant by addition of de Morgan laws
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-23 paulson 1996-09-23 Addition of le_refl to default simpset/claset
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-08-21 paulson 1996-08-21 Added le_eq_less_Suc; fixed some comments; a bit of tidying up
1996-08-19 paulson 1996-08-19 Now less_zeroE is a Safe Elim rule
1996-06-25 berghofe 1996-06-25 Changed argument order of nat_rec.
1996-06-21 berghofe 1996-06-21 Replaced occurrence of fast_tac by Fast_tac .
1996-06-20 paulson 1996-06-20 Corrected comment
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-31 oheimb 1996-05-31 renamed le_0 to le_0_eq, to avoid confusion with le0, supplied an experimental thm Suc_le_eq, but commented it out
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-03-04 nipkow 1996-03-04 Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-11-12 nipkow 1995-11-12 added new arithmetic lemmas and the functions take and drop.
1995-10-25 nipkow 1995-10-25 Added various thms and tactics.
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-04-10 nipkow 1995-04-10 ROOT.ML: installed new hyp_subst_tac Nat.ML: Changed proof of lessE for new hyp_subst_tac
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-17 nipkow 1995-03-17 Added a few thms to nat_ss and list_ss
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application