# HG changeset patch
# User huffman
# Date 1228345250 28800
# Node ID 9d35303719b5cc72209a190afa03c7a794d625e5
# Parent  74c60b78969c7e6f518626a2e161e470332c1cce
fixed proofs due to changes in Int.thy

diff -r 74c60b78969c -r 9d35303719b5 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Wed Dec 03 14:23:03 2008 -0800
+++ b/src/HOL/Word/BinGeneral.thy	Wed Dec 03 15:00:50 2008 -0800
@@ -371,25 +371,12 @@
 lemma bin_rec_Bit0:
   "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
     bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
-  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
-  unfolding Pls_def Min_def Bit0_def
-  apply auto
-  apply presburger
-  apply (simp add: bin_rec.simps)
-  done
+  by (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
 
 lemma bin_rec_Bit1:
   "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
     bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
-  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
-  unfolding Pls_def Min_def Bit1_def
-  apply auto
-  apply (cases w)
-  apply auto
-  apply (simp add: bin_rec.simps)
-    unfolding Min_def Pls_def number_of_is_id apply auto
-  unfolding Bit0_def apply presburger
-  done
+  by (simp add: bin_rec_Min bin_rec.simps [of _ _ _ "Int.Bit1 w"])
   
 lemma bin_rec_Bit:
   "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
diff -r 74c60b78969c -r 9d35303719b5 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Wed Dec 03 14:23:03 2008 -0800
+++ b/src/HOL/Word/WordArith.thy	Wed Dec 03 15:00:50 2008 -0800
@@ -395,8 +395,7 @@
 
 lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
   unfolding word_arith_wis
-  apply (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
-  unfolding Bit0_def Bit1_def by simp
+  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
 
 lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
 
@@ -1254,4 +1253,3 @@
 unfolding word_size by (rule card_word)
 
 end 
-