--- a/src/HOL/Word/Num_Lemmas.thy Tue Aug 21 20:53:37 2007 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy Tue Aug 21 20:59:35 2007 +0200
@@ -10,11 +10,6 @@
lemma contentsI: "y = {x} ==> contents y = x"
unfolding contents_def by auto
-lemma prod_case_split: "prod_case = split"
- by (rule ext)+ auto
-
-lemmas split_split = prod.split [unfolded prod_case_split]
-lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
lemmas "split.splits" = split_split split_split_asm
lemmas funpow_0 = funpow.simps(1)
@@ -32,8 +27,6 @@
mod_alt :: "'a => 'a => 'a :: Divides.div"
"mod_alt n m == n mod m"
-declare iszero_0 [iff]
-
lemmas xtr1 = xtrans(1)
lemmas xtr2 = xtrans(2)
lemmas xtr3 = xtrans(3)
@@ -71,10 +64,6 @@
apply (simp add: number_of_eq nat_diff_distrib [symmetric])
done
-lemma of_int_power:
- "of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})"
- by (induct n) (auto simp add: power_Suc)
-
lemma zless2: "0 < (2 :: int)"
by auto