src/HOL/Word/Bool_List_Representation.thy

--- a/src/HOL/Word/Bool_List_Representation.thy	Sun Nov 20 20:26:13 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Sun Nov 20 20:59:30 2011 +0100
@@ -301,7 +301,7 @@
   apply arith
   done
 
-lemmas nth_rev_alt = nth_rev [where xs = "rev ys", simplified, standard]
+lemmas nth_rev_alt = nth_rev [where xs = "rev ys", simplified] for ys
 
 lemma nth_bin_to_bl_aux [rule_format] : 
   "ALL w n bl. n < m + length bl --> (bin_to_bl_aux m w bl) ! n = 
@@ -361,7 +361,7 @@
   done
 
 lemmas butlast_bin_rest = butlast_rest_bin
-  [where w="bl_to_bin bl" and n="length bl", simplified, standard]
+  [where w="bl_to_bin bl" and n="length bl", simplified] for bl
 
 lemma butlast_rest_bl2bin_aux:
   "bl ~= [] \<Longrightarrow>
@@ -401,7 +401,7 @@
   unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
   
 lemmas trunc_bl2bin_len [simp] =
-  trunc_bl2bin [of "length bl" bl, simplified, standard]  
+  trunc_bl2bin [of "length bl" bl, simplified] for bl
 
 lemma bl2bin_drop: 
   "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
@@ -634,16 +634,16 @@
   by auto
 
 lemmas takefill_Suc_cases = 
-  list.cases [THEN takefill.Suc [THEN trans], standard]
+  list.cases [THEN takefill.Suc [THEN trans]]
 
 lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
 lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
 
 lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] 
-  takefill_minus [symmetric, THEN trans], standard]
+  takefill_minus [symmetric, THEN trans]]
 
 lemmas takefill_pred_simps [simp] =
-  takefill_minus_simps [where n="number_of bin", simplified nobm1, standard]
+  takefill_minus_simps [where n="number_of bin", simplified nobm1] for bin
 
 (* links with function bl_to_bin *)
 
@@ -927,7 +927,7 @@
 
 lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
 
-lemmas seqr = eq_reflection [where x = "size w", standard]
+lemmas seqr = eq_reflection [where x = "size w"] for w
 
 lemmas tl_Nil = tl.simps (1)
 lemmas tl_Cons = tl.simps (2)
@@ -966,10 +966,8 @@
 lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
 lemmas rsplit_aux_simps = bin_rsplit_aux_simps
 
-lemmas th_if_simp1 = split_if [where P = "op = l",
-  THEN iffD1, THEN conjunct1, THEN mp, standard]
-lemmas th_if_simp2 = split_if [where P = "op = l",
-  THEN iffD1, THEN conjunct2, THEN mp, standard]
+lemmas th_if_simp1 = split_if [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l
+lemmas th_if_simp2 = split_if [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l
 
 lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
 
@@ -1011,7 +1009,7 @@
   by auto
 
 lemmas bin_split_minus_simp =
-  bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans], standard]
+  bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]]
 
 lemma bin_split_pred_simp [simp]: 
   "(0::nat) < number_of bin \<Longrightarrow>
@@ -1034,8 +1032,7 @@
   done
 
 lemmas bin_rsplit_simp_alt = 
-  trans [OF bin_rsplit_def
-            bin_rsplit_aux_simp_alt, standard]
+  trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt]
 
 lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
 
@@ -1054,8 +1051,7 @@
   done
 
 lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl 
-  rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]],
-  standard]
+  rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]]
 
 lemma bin_nth_rsplit [rule_format] :
   "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) -->