src/HOL/Nat.thy
2007-09-26 haftmann 2007-09-26 added code lemma for 1
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-03 nipkow 2007-09-03 added variations on infinite descent
2007-08-27 nipkow 2007-08-27 Added infinite_descent
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-09 haftmann 2007-08-09 localized of_nat
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-07-31 wenzelm 2007-07-31 added Tools/lin_arith.ML;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-19 haftmann 2007-07-19 moved set Nats to Nat.thy
2007-07-11 berghofe 2007-07-11 Adapted to new package for inductive sets.
2007-06-22 huffman 2007-06-22 fix looping simp rule
2007-06-20 huffman 2007-06-20 remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
2007-06-20 huffman 2007-06-20 change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-12 huffman 2007-06-12 add lemma inj_of_nat
2007-06-06 huffman 2007-06-06 add axclass semiring_char_0 for types where of_nat is injective
2007-06-06 huffman 2007-06-06 generalize of_nat and related constants to class semiring_1
2007-06-05 haftmann 2007-06-05 tuned boostrap
2007-05-17 krauss 2007-05-17 added induction principles for induction "backwards": P (Suc n) ==> P n
2007-05-10 haftmann 2007-05-10 size [nat] is identity
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-04-17 wenzelm 2007-04-17 tuned proofs;
2007-03-20 haftmann 2007-03-20 added instance for lattice
2007-03-20 haftmann 2007-03-20 explizit "type" superclass
2007-02-23 haftmann 2007-02-23 adjusted code lemmas
2007-02-14 haftmann 2007-02-14 simpliefied instance statement
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2007-01-26 paulson 2007-01-26 min/max lemmas (actually unused!)
2007-01-22 krauss 2007-01-22 Added lemma nat_size[simp]: "size (n::nat) = n"
2006-12-06 wenzelm 2006-12-06 added aliases for nat_recs/cases;
2006-11-22 haftmann 2006-11-22 cleanup
2006-11-18 haftmann 2006-11-18 power is now a class
2006-11-08 wenzelm 2006-11-08 removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
2006-11-06 haftmann 2006-11-06 code generator module naming improved
2006-10-16 haftmann 2006-10-16 added explicit print translation for nat_case
2006-10-02 haftmann 2006-10-02 added code generator names for nat_rec and nat_case
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-25 haftmann 2006-09-25 refinements in codegen serializer
2006-09-20 haftmann 2006-09-20 name shifts
2006-09-19 haftmann 2006-09-19 added operational equality
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-08-08 haftmann 2006-08-08 cleanup code generation for Numerals
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-13 paulson 2006-06-13 new results
2006-05-05 wenzelm 2006-05-05 axiomatization;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-11 paulson 2006-01-11 tidied, and giving theorems names
2005-09-29 wenzelm 2005-09-29 more finalconsts;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-07-01 berghofe 2005-07-01 Moved some code lemmas from Main to Nat.
2005-05-04 nipkow 2005-05-04 Fixing a problem with lin.arith.
2005-02-21 nipkow 2005-02-21 comprehensive cleanup, replacing sumr by setsum
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
2004-11-13 nipkow 2004-11-13 More lemmas
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct