src/HOL/Nat.thy
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-28 haftmann 2007-11-28 dropped implicit assumption proof
2007-11-10 wenzelm 2007-11-10 tuned specifications of 'notation';
2007-10-30 haftmann 2007-10-30 simplified proof
2007-10-25 haftmann 2007-10-25 various localizations
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-23 paulson 2007-10-23 random tidying of proofs
2007-10-22 haftmann 2007-10-22 dropped superfluous inlining lemmas
2007-10-21 nipkow 2007-10-21 More changes from >0 to ~=0::nat
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-20 chaieb 2007-10-20 neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
2007-10-18 haftmann 2007-10-18 localized mono predicate
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-12 haftmann 2007-10-12 refined; moved class power to theory Power
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