src/HOL/Nat.ML
2005-05-04 nipkow 2005-05-04 Fixing a problem with lin.arith.
2004-12-15 paulson 2004-12-15 removal of archaic Abs/Rep proofs
2004-11-29 paulson 2004-11-29 converted to Isar script, simplifying some results
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2002-08-05 berghofe 2002-08-05 Legacy ML bindings.
2002-07-31 nipkow 2002-07-31 added mk_left_commute to HOL.thy and used it "everywhere"
2002-04-25 nipkow 2002-04-25 added "m <= n ==> m-n = 0" [simp]
2002-02-26 paulson 2002-02-26 Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and return False for e.g. Suc x = 0. Removed ad-hoc lemmas for that purpose.
2002-02-25 nipkow 2002-02-25 solved the problem that Larry's simproce cancle_numerals(?) returns inconsistent inequality w/o rewriting it to False.
2001-12-13 wenzelm 2001-12-13 isatool expandshort;
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-06 nipkow 2001-08-06 turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.
2001-05-31 oheimb 2001-05-31 added Least_Suc2
2001-02-15 oheimb 2001-02-15 moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least from Nat.ML to Wellfounded_Recursion.ML moved Least_equality from Nat.ML to Ord.thy moved wf_less from Nat.ML to NatDef.ML added wellorder axclass nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy
2001-01-10 paulson 2001-01-10 generalizing the LEAST theorems from "nat" to linear orderings and wellorderings
2000-12-20 paulson 2000-12-20 tidying, removing obsolete lemmas about 0=... and 1=...
2000-12-01 paulson 2000-12-01 renamed less_eq_Suc_add to less_imp_Suc_add
2000-11-10 wenzelm 2000-11-10 nat_distrib;
2000-10-09 paulson 2000-10-09 got rid of a swap
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-06 nipkow 2000-09-06 less_induct -> nat_less_induct
2000-08-17 paulson 2000-08-17 better rules for cancellation of common factors across comparisons
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-03-13 wenzelm 2000-03-13 case_tac now subsumes both boolean and datatype cases;
2000-03-13 nipkow 2000-03-13 exhaust_tac -> cases_tac
2000-02-18 oheimb 2000-02-18 added Suc_le_D
2000-01-10 nipkow 2000-01-10 Forgot to "call" MicroJava in makefile. Added list_all2 to List.
1999-07-27 paulson 1999-07-27 expandshort and tidying
1999-07-21 paulson 1999-07-21 removed 2 qed_goals
1999-06-10 paulson 1999-06-10 new lemma less_Suc_eq_0_disj
1999-04-15 nipkow 1999-04-15 Added new thms.
1999-03-03 paulson 1999-03-03 expandshort
1999-01-13 nipkow 1999-01-13 Refined arithmetic.
1999-01-13 nipkow 1999-01-13 Simplified arithmetic.
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-10-14 nipkow 1998-10-14 Nat: added zero_neq_conv List: added nth/update lemmas.
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
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.