2009-02-24 huffman [Tue, 24 Feb 2009 11:12:58 -0800] rev 30082
make more proofs work whether or not One_nat_def is a simp rule
src/HOL/Fact.thy src/HOL/GCD.thy src/HOL/Integration.thy src/HOL/MacLaurin.thy src/HOL/RealDef.thy src/HOL/RealPow.thy src/HOL/SEQ.thy src/HOL/Series.thy src/HOL/Transcendental.thy

2009-02-24 huffman [Tue, 24 Feb 2009 11:10:05 -0800] rev 30081
add simp rules for numerals with 1::nat
src/HOL/NatBin.thy

2009-02-24 huffman [Tue, 24 Feb 2009 08:20:14 -0800] rev 30080
fix lemma hypreal_hnorm_def
src/HOL/NSA/NSA.thy

2009-02-23 huffman [Mon, 23 Feb 2009 16:25:52 -0800] rev 30079
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
src/HOL/Arith_Tools.thy src/HOL/Divides.thy src/HOL/Groebner_Basis.thy src/HOL/Int.thy src/HOL/IntDiv.thy src/HOL/List.thy src/HOL/Nat.thy src/HOL/NatBin.thy src/HOL/Power.thy src/HOL/Relation_Power.thy src/HOL/SetInterval.thy

2009-02-23 huffman [Mon, 23 Feb 2009 13:55:36 -0800] rev 30078
move lemma dvd_mod_imp_dvd into class semiring_div
src/HOL/Divides.thy

2009-02-23 haftmann [Mon, 23 Feb 2009 21:38:45 +0100] rev 30077
merged

2009-02-23 haftmann [Mon, 23 Feb 2009 21:38:36 +0100] rev 30076
improved treatment of case certificates
src/HOL/Tools/datatype_codegen.ML src/Pure/Isar/code.ML

2009-02-23 haftmann [Mon, 23 Feb 2009 21:34:14 +0100] rev 30075
repaired order of variable node allocation
src/Tools/code/code_wellsorted.ML

2009-02-23 huffman [Mon, 23 Feb 2009 10:42:31 -0800] rev 30074
explicitly import Fact
src/HOL/Library/Permutations.thy

2009-02-23 huffman [Mon, 23 Feb 2009 07:58:13 -0800] rev 30073
change imports to move Fact.thy outside Plain
src/HOL/Fact.thy src/HOL/Plain.thy