# HG changeset patch
# User huffman
# Date 1187722775 -7200
# Node ID de9997397317fc23276b08292c3a87dad65d58e8
# Parent  b9718519f3d227394a2b2f261440d5b821d8293f
remove redundant lemmas

diff -r b9718519f3d2 -r de9997397317 src/HOL/Word/Num_Lemmas.thy
--- 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