Tue, 24 Feb 2009 11:10:05 -0800 add simp rules for numerals with 1::nat
huffman [Tue, 24 Feb 2009 11:10:05 -0800] rev 30081
add simp rules for numerals with 1::nat
Tue, 24 Feb 2009 08:20:14 -0800 fix lemma hypreal_hnorm_def
huffman [Tue, 24 Feb 2009 08:20:14 -0800] rev 30080
fix lemma hypreal_hnorm_def
Mon, 23 Feb 2009 16:25:52 -0800 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
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
Mon, 23 Feb 2009 13:55:36 -0800 move lemma dvd_mod_imp_dvd into class semiring_div
huffman [Mon, 23 Feb 2009 13:55:36 -0800] rev 30078
move lemma dvd_mod_imp_dvd into class semiring_div
Mon, 23 Feb 2009 21:38:45 +0100 merged
haftmann [Mon, 23 Feb 2009 21:38:45 +0100] rev 30077
merged
Mon, 23 Feb 2009 21:38:36 +0100 improved treatment of case certificates
haftmann [Mon, 23 Feb 2009 21:38:36 +0100] rev 30076
improved treatment of case certificates
Mon, 23 Feb 2009 21:34:14 +0100 repaired order of variable node allocation
haftmann [Mon, 23 Feb 2009 21:34:14 +0100] rev 30075
repaired order of variable node allocation
Mon, 23 Feb 2009 10:42:31 -0800 explicitly import Fact
huffman [Mon, 23 Feb 2009 10:42:31 -0800] rev 30074
explicitly import Fact
Mon, 23 Feb 2009 07:58:13 -0800 change imports to move Fact.thy outside Plain
huffman [Mon, 23 Feb 2009 07:58:13 -0800] rev 30073
change imports to move Fact.thy outside Plain
Mon, 23 Feb 2009 07:19:53 -0800 add lemmas poly_{div,mod}_minus_{left,right}
huffman [Mon, 23 Feb 2009 07:19:53 -0800] rev 30072
add lemmas poly_{div,mod}_minus_{left,right}
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip