# HG changeset patch
# User huffman
# Date 1330098403 -3600
# Node ID bec50f8b372796d1449a390ce700dfbfd36be339
# Parent  689ebcbd634392a4a2b48d713521a5d0011bede1
avoid using BIT_simps in proofs

diff -r 689ebcbd6343 -r bec50f8b3727 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 13:50:37 2012 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 16:46:43 2012 +0100
@@ -331,9 +331,8 @@
    apply clarsimp
   apply clarsimp
   apply safe
-   apply (drule meta_spec, erule preorder_class.order_trans [rotated],
-          simp add: numeral_simps algebra_simps BIT_simps
-          cong add: number_of_False_cong)+
+   apply (drule meta_spec, erule order_trans [rotated],
+          simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+
   done
 
 lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
@@ -377,14 +376,14 @@
   apply safe
    apply (case_tac "m - size bl")
     apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
-   apply (simp add: BIT_simps)
-   apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit1 (bintrunc nat w))" 
+   apply simp
+   apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 1)" 
                    in arg_cong)
    apply simp
   apply (case_tac "m - size bl")
    apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
-  apply (simp add: BIT_simps)
-  apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit0 (bintrunc nat w))" 
+  apply simp
+  apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 0)"
                   in arg_cong)
   apply simp
   done