# HG changeset patch
# User wenzelm
# Date 1321819523 -3600
# Node ID a89b4bc311a53064ebcab25bbbc064b0449aed58
# Parent  29cf40fe8daf2804a51a8ada9eaf8266c2d7da18
eliminated obsolete "standard";

diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/Event.thy
--- a/src/HOL/Auth/Event.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Event.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -93,7 +93,7 @@
 (*Simplifying   
  parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
   This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
 
 lemma knows_Spy_Says [simp]:
      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -138,10 +138,10 @@
 text{*Elimination rules: derive contradictions from old Says events containing
   items known to be fresh*}
 lemmas Says_imp_parts_knows_Spy = 
-       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
+       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl] 
 
 lemmas knows_Spy_partsEs =
-     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
+     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl]
 
 lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
 
@@ -278,7 +278,7 @@
     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
 
 
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
 
 ML
 {*
@@ -294,7 +294,7 @@
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
 
-lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
+lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
 
 ML
 {*
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Message.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -166,7 +166,7 @@
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
@@ -358,9 +358,9 @@
 apply (erule analz.induct, blast+)
 done
 
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -371,7 +371,7 @@
 apply (erule analz.induct, auto)
 done
 
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection{*General equational properties *}
 
@@ -790,21 +790,23 @@
 text{*Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the @{text analz_insert} rules*}
 
-lemmas pushKeys [standard] =
+lemmas pushKeys =
   insert_commute [of "Key K" "Agent C"]
   insert_commute [of "Key K" "Nonce N"]
   insert_commute [of "Key K" "Number N"]
   insert_commute [of "Key K" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
+  for K C N X Y K'
 
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Nonce N"]
   insert_commute [of "Crypt X K" "Number N"]
   insert_commute [of "Crypt X K" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
+  for X K C N X' Y
 
 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   re-ordered. *}
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/OtwayRees.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -121,7 +121,7 @@
   We can replace them by rewriting with parts_insert2 and proving using
   dest: parts_cut, but the proofs become more difficult.*)
 lemmas OR2_parts_knows_Spy =
-    OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+    OR2_analz_knows_Spy [THEN analz_into_parts]
 
 (*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for
   some reason proofs work without them!*)
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/OtwayReesBella.thy
--- a/src/HOL/Auth/OtwayReesBella.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -122,7 +122,7 @@
 by blast
 
 lemmas OR2_parts_knows_Spy =
-    OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+    OR2_analz_knows_Spy [THEN analz_into_parts]
 
 ML
 {*
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -128,7 +128,7 @@
 
 text{*Forwarding lemma: see comments in OtwayRees.thy*}
 lemmas OR2_parts_knows_Spy =
-    OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+    OR2_analz_knows_Spy [THEN analz_into_parts]
 
 
 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/Smartcard/EventSC.thy
--- a/src/HOL/Auth/Smartcard/EventSC.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -118,7 +118,7 @@
 (*Simplifying   
  parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
   This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
 
 lemma knows_Spy_Says [simp]:
      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -237,8 +237,8 @@
 text{*Elimination rules: derive contradictions from old Says events containing
   items known to be fresh*}
 lemmas knows_Spy_partsEs =
-     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
-     parts.Body [THEN revcut_rl, standard]
+     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
+     parts.Body [THEN revcut_rl]
 
 
 
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -121,7 +121,7 @@
 by blast
 
 lemmas YM4_parts_knows_Spy =
-       YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+       YM4_analz_knows_Spy [THEN analz_into_parts]
 
 text{*For Oops*}
 lemma YM4_Key_parts_knows_Spy:
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Yahalom2.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -116,7 +116,7 @@
 by blast
 
 lemmas YM4_parts_knows_Spy =
-       YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+       YM4_analz_knows_Spy [THEN analz_into_parts]
 
 
 (** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Auth/Yahalom_Bad.thy
--- a/src/HOL/Auth/Yahalom_Bad.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Yahalom_Bad.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -103,7 +103,7 @@
 by blast
 
 lemmas YM4_parts_knows_Spy =
-       YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+       YM4_analz_knows_Spy [THEN analz_into_parts]
 
 
 text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -30,7 +30,7 @@
 done
 
 lemmas finite_nyinitcls [simp] =
-   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
+   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset]]
 
 lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
 apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/AxSem.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -1016,7 +1016,7 @@
 apply  (rule ax_derivs.Skip)
 apply fast
 done
-lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
+lemmas ax_SkipI = ax_Skip [THEN conseq1]
 
 
 section "derived rules for methd call"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/Decl.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -613,8 +613,8 @@
 apply auto
 done
 
-lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
-lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
+lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI]
+lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI]
 
 
 lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/Table.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -222,7 +222,7 @@
 apply auto
 done
 
-lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]
+lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI]
 
 lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
    table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -60,7 +60,7 @@
   (* direct subinterface in Decl.thy, cf. 9.1.3 *)
   (* direct subclass     in Decl.thy, cf. 8.1.3 *)
 
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
 
 lemma subcls_direct1:
  "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D"
@@ -554,9 +554,9 @@
 done
 
 lemmas subint_antisym = 
-       subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
+       subint1_acyclic [THEN acyclic_impl_antisym_rtrancl]
 lemmas subcls_antisym = 
-       subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
+       subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl]
 
 lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
 by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/WellForm.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -739,7 +739,7 @@
 proof -
   assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
 
-  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
+  note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]  (* FIXME !? *)
   have "wf_prog G \<longrightarrow> 
          (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
                   \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
@@ -1355,7 +1355,7 @@
   qed
 qed
 
-lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
+lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P
 
 lemma declclass_widen[rule_format]: 
  "wf_prog G 
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -281,7 +281,7 @@
 apply (drule_tac x = m in spec)
 apply (auto simp add:field_simps)
 done
-lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0, standard]
+lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0]
 
 lemma poly_roots_index_length0: "poly p (x::'a::idom) \<noteq> poly [] x ==>
       \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)"
@@ -322,7 +322,7 @@
 apply (clarsimp simp add: field_simps)
 done
 
-lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
+lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma]
 
 lemma poly_roots_index_length: "poly p (x::'a::idom) \<noteq> poly [] x ==>
       \<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -24,7 +24,7 @@
   elements of the chain.
 *}
 lemmas [dest?] = chainD
-lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
+lemmas chainE2 [elim?] = chainD2 [elim_format]
 
 lemma some_H'h't:
   assumes M: "M = norm_pres_extensions E p F f"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/IMP/Comp_Rev.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -363,7 +363,7 @@
 qed
 
 lemmas exec_n_drop_Cons = 
-  exec_n_drop_left [where P="[instr]", simplified, standard]
+  exec_n_drop_left [where P="[instr]", simplified] for instr
 
 definition
   "closed P \<longleftrightarrow> exits P \<subseteq> {isize P}" 
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/IMPP/Hoare.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -460,7 +460,7 @@
 done
 
 (* requires Body+empty+insert / BodyN, com_det *)
-lemmas hoare_complete = MGF' [THEN MGF_complete, standard]
+lemmas hoare_complete = MGF' [THEN MGF_complete]
 
 
 subsection "unused derived rules"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Induct/PropLog.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -111,7 +111,7 @@
 
 lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
 
-lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
+lemmas thms_notE = thms.MP [THEN thms_falseE]
 
 
 subsubsection {* Soundness of the rules wrt truth-table semantics *}
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Induct/SList.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -191,7 +191,7 @@
 by (simp add: NIL_def CONS_def)
 
 lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
-lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
+lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE]
 lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
 
 lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
@@ -200,8 +200,9 @@
 apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
 done
 
-lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
-lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
+lemmas Nil_not_Cons = Cons_not_Nil [THEN not_sym]
+declare Nil_not_Cons [iff]
+lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE]
 lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
 
 (** Injectiveness of CONS and Cons **)
@@ -220,7 +221,7 @@
 apply (auto simp add: Rep_List_inject)
 done
 
-lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
+lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
 
 lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
   by (induct L == "CONS M N" set: list) auto
@@ -264,8 +265,7 @@
 by (simp add: List_rec_def)
 
 lemmas List_rec_unfold = 
-    def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl], 
-               standard]
+    def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl]]
 
 
 (** pred_sexp lemmas **)
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Library/AList.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -467,7 +467,7 @@
   (map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
   by (simp add: merge_conv' map_add_Some_iff)
 
-lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
+lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
 
 lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   by (simp add: merge_conv')
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -928,11 +928,9 @@
 lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
 by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
 
-lemmas pdivmod_rel_unique_div =
-  pdivmod_rel_unique [THEN conjunct1, standard]
+lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
 
-lemmas pdivmod_rel_unique_mod =
-  pdivmod_rel_unique [THEN conjunct2, standard]
+lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
 
 instantiation poly :: (field) ring_div
 begin
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -164,7 +164,7 @@
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
@@ -353,9 +353,9 @@
 apply (erule analz.induct, blast+)
 done
 
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
@@ -369,7 +369,7 @@
 apply (erule analz.induct, auto)
 done
 
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection{*General equational properties *}
 
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -142,7 +142,7 @@
 apply (case_tac t)
  apply simp
 apply simp
-apply (insert rtrancl_r_diff_Id [symmetric, standard, of "subcls1 G"])
+apply (insert rtrancl_r_diff_Id [symmetric, of "subcls1 G"])
 apply simp
 apply (erule rtrancl.cases)
  apply blast
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -202,7 +202,7 @@
 apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
 done
 
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"], standard]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"]] for G
 
 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
 apply (rule subcls_direct)
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -141,22 +141,22 @@
   done
 
 lemmas scaleR_right_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
 
 lemmas scaleR_left_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
+  bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
 
 lemmas inner_right_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
+  bounded_linear.has_derivative [OF bounded_linear_inner_right]
 
 lemmas inner_left_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
+  bounded_linear.has_derivative [OF bounded_linear_inner_left]
 
 lemmas mult_right_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
+  bounded_linear.has_derivative [OF bounded_linear_mult_right]
 
 lemmas mult_left_has_derivative =
-  bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
+  bounded_linear.has_derivative [OF bounded_linear_mult_left]
 
 lemmas euclidean_component_has_derivative =
   bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/NSA/Examples/NSPrimes.thy
--- a/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -39,7 +39,7 @@
 apply (force intro!: dvd_mult)
 done
 
-lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard]
+lemmas dvd_by_all2 = dvd_by_all [THEN spec]
 
 lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
 by (transfer, simp)
@@ -50,7 +50,7 @@
 lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
 by (transfer, rule dvd_by_all)
 
-lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
+lemmas hdvd_by_all2 = hdvd_by_all [THEN spec]
 
 (* Goldblatt: Exercise 5.11(2) - p. 57 *)
 lemma hypnat_dvd_all_hypnat_of_nat:
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -422,7 +422,7 @@
 lemma power_hypreal_of_real_number_of:
      "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
 by simp
-declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
+declare power_hypreal_of_real_number_of [of _ "number_of w", simp] for w
 (*
 lemma hrealpow_HFinite:
   fixes x :: "'a::{real_normed_algebra,power} star"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -683,18 +683,18 @@
 text{*As above, for numerals*}
 
 lemmas star_of_number_less =
-  star_of_less [of "number_of w", standard, simplified star_of_number_of]
+  star_of_less [of "number_of w", simplified star_of_number_of] for w
 lemmas star_of_number_le   =
-  star_of_le   [of "number_of w", standard, simplified star_of_number_of]
+  star_of_le   [of "number_of w", simplified star_of_number_of] for w
 lemmas star_of_number_eq   =
-  star_of_eq   [of "number_of w", standard, simplified star_of_number_of]
+  star_of_eq   [of "number_of w", simplified star_of_number_of] for w
 
 lemmas star_of_less_number =
-  star_of_less [of _ "number_of w", standard, simplified star_of_number_of]
+  star_of_less [of _ "number_of w", simplified star_of_number_of] for w
 lemmas star_of_le_number   =
-  star_of_le   [of _ "number_of w", standard, simplified star_of_number_of]
+  star_of_le   [of _ "number_of w", simplified star_of_number_of] for w
 lemmas star_of_eq_number   =
-  star_of_eq   [of _ "number_of w", standard, simplified star_of_number_of]
+  star_of_eq   [of _ "number_of w", simplified star_of_number_of] for w
 
 lemmas star_of_simps [simp] =
   star_of_add     star_of_diff    star_of_minus
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -196,6 +196,6 @@
 apply (auto del: image_eqI intro: rev_image_eqI)
 done
 
-lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard]
+lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified] for Cm
 
 end
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -86,7 +86,7 @@
 apply auto
 done
 
-lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
+lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI]
 
 lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
 by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -206,7 +206,7 @@
     "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
   by (auto simp add: prime_nat_code)
 
-lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
+lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m"] for m
 
 lemma prime_int_code [code]:
   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
@@ -222,7 +222,7 @@
 lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
   by (auto simp add: prime_int_code)
 
-lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
+lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m"] for m
 
 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   by simp
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -196,10 +196,8 @@
   apply (rule aux_some, simp_all)
   done
 
-lemmas RRset2norRR_correct1 =
-  RRset2norRR_correct [THEN conjunct1, standard]
-lemmas RRset2norRR_correct2 =
-  RRset2norRR_correct [THEN conjunct2, standard]
+lemmas RRset2norRR_correct1 = RRset2norRR_correct [THEN conjunct1]
+lemmas RRset2norRR_correct2 = RRset2norRR_correct [THEN conjunct2]
 
 lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
   by (induct set: RsetR) auto
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Old_Number_Theory/WilsonBij.thy
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -41,9 +41,9 @@
     apply auto
   done
 
-lemmas inv_ge = inv_correct [THEN conjunct1, standard]
-lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1, standard]
-lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2, standard]
+lemmas inv_ge = inv_correct [THEN conjunct1]
+lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1]
+lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2]
 
 lemma inv_not_0:
   "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Proofs/Lambda/NormalForm.thy
--- a/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -132,10 +132,10 @@
   apply (drule listall_conj2)
   apply (drule_tac i=i and j=j in subst_terms_NF)
   apply assumption
-  apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard])
+  apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
   apply simp
   apply (erule NF.App)
-  apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
+  apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
   apply simp
   apply (iprover intro: NF.App)
   apply simp
@@ -173,7 +173,7 @@
   apply (drule listall_conj2)
   apply (drule_tac i=i in lift_terms_NF)
   apply assumption
-  apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard])
+  apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
   apply simp
   apply (rule NF.App)
   apply assumption
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -649,8 +649,8 @@
 subsection {* union_fset *}
 
 lemmas [simp] =
-  sup_bot_left[where 'a="'a fset", standard]
-  sup_bot_right[where 'a="'a fset", standard]
+  sup_bot_left[where 'a="'a fset"]
+  sup_bot_right[where 'a="'a fset"]
 
 lemma union_insert_fset [simp]:
   shows "insert_fset x S |\<union>| T = insert_fset x (S |\<union>| T)"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -263,11 +263,12 @@
 qed
 
 lemmas int_distrib =
-  left_distrib [of "z1::int" "z2" "w", standard]
-  right_distrib [of "w::int" "z1" "z2", standard]
-  left_diff_distrib [of "z1::int" "z2" "w", standard]
-  right_diff_distrib [of "w::int" "z1" "z2", standard]
-  minus_add_distrib[of "z1::int" "z2", standard]
+  left_distrib [of z1 z2 w]
+  right_distrib [of w z1 z2]
+  left_diff_distrib [of z1 z2 w]
+  right_diff_distrib [of w z1 z2]
+  minus_add_distrib[of z1 z2]
+  for z1 z2 w :: int
 
 lemma int_induct_raw:
   assumes a: "P (0::nat, 0)"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/SET_Protocol/Event_SET.thy
--- a/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -82,7 +82,7 @@
 (** Simplifying   parts (insert X (knows Spy evs))
       = parts {X} Un parts (knows Spy evs) -- since general case loops*)
 
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
 
 lemma knows_Spy_Says [simp]:
      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -126,8 +126,8 @@
 (*Use with addSEs to derive contradictions from old Says events containing
   items known to be fresh*)
 lemmas knows_Spy_partsEs =
-     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
-     parts.Body [THEN revcut_rl, standard]
+     Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl] 
+     parts.Body [THEN revcut_rl]
 
 
 subsection{*The Function @{term used}*}
@@ -177,7 +177,7 @@
        knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
        knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
 
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
 
 ML
 {*
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -210,7 +210,7 @@
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
@@ -424,9 +424,9 @@
 apply (erule analz.induct, blast+)
 done
 
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
 
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -440,7 +440,7 @@
 apply (erule analz.induct, auto)
 done
 
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection{*General equational properties*}
 
@@ -811,7 +811,7 @@
 text{*Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the @{text analz_insert} rules*}
 
-lemmas pushKeys [standard] =
+lemmas pushKeys =
   insert_commute [of "Key K" "Agent C"]
   insert_commute [of "Key K" "Nonce N"]
   insert_commute [of "Key K" "Number N"]
@@ -819,14 +819,16 @@
   insert_commute [of "Key K" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
+  for K C N PAN X Y K'
 
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Nonce N"]
   insert_commute [of "Crypt X K" "Number N"]
   insert_commute [of "Crypt X K" "Pan PAN"]
   insert_commute [of "Crypt X K" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
+  for X K C N PAN X' Y
 
 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   re-ordered.*}
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -819,7 +819,7 @@
   apply force
   done
 (* turn into (unsafe, looping!) introduction rule *)
-lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard]
+lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
 
 lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/TLA/TLA.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -149,7 +149,7 @@
 section "Simple temporal logic"
 
 (* []~F == []~Init F *)
-lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps, standard]
+lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F
 
 lemma dmdInit: "TEMP <>F == TEMP <> Init F"
   apply (unfold dmd_def)
@@ -157,15 +157,15 @@
   apply (simp (no_asm) add: Init_simps)
   done
 
-lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps, standard]
+lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F
 
 (* boxInit and dmdInit cannot be used as rewrites, because they loop.
    Non-looping instances for state predicates and actions are occasionally useful.
 *)
-lemmas boxInit_stp = boxInit [where 'a = state, standard]
-lemmas boxInit_act = boxInit [where 'a = "state * state", standard]
-lemmas dmdInit_stp = dmdInit [where 'a = state, standard]
-lemmas dmdInit_act = dmdInit [where 'a = "state * state", standard]
+lemmas boxInit_stp = boxInit [where 'a = state]
+lemmas boxInit_act = boxInit [where 'a = "state * state"]
+lemmas dmdInit_stp = dmdInit [where 'a = state]
+lemmas dmdInit_act = dmdInit [where 'a = "state * state"]
 
 (* The symmetric equations can be used to get rid of Init *)
 lemmas boxInitD = boxInit [symmetric]
@@ -208,14 +208,14 @@
    [| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
 *)
 lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
-lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1, standard]
+lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
 
 (* dual versions for <> *)
 lemma DmdDmd: "|- (<><>F) = (<>F)"
   by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
 
 lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
-lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1, standard]
+lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1]
 
 
 (* ------------------------ STL4 ------------------------------------------- *)
@@ -266,7 +266,7 @@
   done
 
 (* rewrite rule to split conjunctions under boxes *)
-lemmas split_box_conj = STL5 [temp_unlift, symmetric, standard]
+lemmas split_box_conj = STL5 [temp_unlift, symmetric]
 
 
 (* the corresponding elimination rule allows to combine boxes in the hypotheses
@@ -283,9 +283,9 @@
 (* Instances of box_conjE for state predicates, actions, and temporals
    in case the general rule is "too polymorphic".
 *)
-lemmas box_conjE_temp = box_conjE [where 'a = behavior, standard]
-lemmas box_conjE_stp = box_conjE [where 'a = state, standard]
-lemmas box_conjE_act = box_conjE [where 'a = "state * state", standard]
+lemmas box_conjE_temp = box_conjE [where 'a = behavior]
+lemmas box_conjE_stp = box_conjE [where 'a = state]
+lemmas box_conjE_act = box_conjE [where 'a = "state * state"]
 
 (* Define a tactic that tries to merge all boxes in an antecedent. The definition is
    a bit kludgy in order to simulate "double elim-resolution".
@@ -318,7 +318,7 @@
 (* rewrite rule to push universal quantification through box:
       (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
 *)
-lemmas all_box = allT [temp_unlift, symmetric, standard]
+lemmas all_box = allT [temp_unlift, symmetric]
 
 lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
   apply (auto simp add: dmd_def split_box_conj [try_rewrite])
@@ -328,7 +328,7 @@
 lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
   by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
 
-lemmas ex_dmd = exT [temp_unlift, symmetric, standard]
+lemmas ex_dmd = exT [temp_unlift, symmetric]
 
 lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
   apply (erule dup_boxE)
@@ -526,7 +526,7 @@
   apply (fastforce elim!: TLA2E [temp_use])
   done
 
-lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use], standard]
+lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use]]
 
 (* ------------------------ INV1, stable --------------------------------------- *)
 section "stable, invariant"
@@ -541,8 +541,8 @@
 lemma box_stp_act: "|- ([]$P) = ([]P)"
   by (simp add: boxInit_act Init_simps)
 
-lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2, standard]
-lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1, standard]
+lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
+lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1]
 
 lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
 
@@ -710,7 +710,7 @@
   done
 
 (* |- F & (F ~> G) --> <>G *)
-lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps, standard]
+lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
 
 lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))"
   apply (unfold leadsto_def)
@@ -776,8 +776,8 @@
     elim!: STL4E_gen [temp_use] simp: Init_simps)
   done
 
-lemmas ImplLeadsto = ImplLeadsto_gen [where 'a = behavior and 'b = behavior,
-  unfolded Init_simps, standard]
+lemmas ImplLeadsto =
+  ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
 
 lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G"
   by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
@@ -1065,7 +1065,7 @@
 
 (* "wf r  ==>  |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *)
 lemmas wf_not_dmd_box_decrease =
-  wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps, standard]
+  wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
 
 (* If there are infinitely many steps where v decreases, then there
    have to be infinitely many non-stuttering steps where v doesn't decrease.
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -791,7 +791,7 @@
   done
 
 lemmas rename_guarantees_sysOfAlloc_I =
-  bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2, standard]
+  bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2]
 
 
 (*Lifting Alloc_Increasing up to the level of systemState*)
@@ -867,7 +867,7 @@
 
 text{*safety (1), step 2*}
 (* i < Nclients ==> System : Increasing (sub i o allocRel) *)
-lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1, standard]
+lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1]
 
 (*Lifting Alloc_safety up to the level of systemState.
   Simplifying with o_def gets rid of the translations but it unfortunately
@@ -921,7 +921,7 @@
 
 text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*}
 (* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
-lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1, standard]
+lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1]
 
 text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
 lemma rename_Client_Bounded: "i : I
@@ -955,7 +955,7 @@
 
 text{*progress (2), step 6*}
 (* i < Nclients ==> System : Increasing (giv o sub i o client) *)
-lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1, standard]
+lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1]
 
 
 lemma rename_Client_Progress: "i: I
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Constrains.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -86,8 +86,7 @@
 
 (*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
 lemmas constrains_reachable_Int =  
-    subset_refl [THEN stable_reachable [unfolded stable_def], 
-                 THEN constrains_Int, standard]
+    subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int]
 
 (*Resembles the previous definition of Constrains*)
 lemma Constrains_eq_constrains: 
@@ -263,8 +262,7 @@
 apply (blast intro: stable_imp_Stable)
 done
 
-lemmas Increasing_constant =  
-    increasing_constant [THEN increasing_imp_Increasing, standard, iff]
+lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
 
 
 subsection{*The Elimination Theorem*}
@@ -294,8 +292,8 @@
 lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
 by (simp add: Always_def)
 
-lemmas AlwaysE = AlwaysD [THEN conjE, standard]
-lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
+lemmas AlwaysE = AlwaysD [THEN conjE]
+lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
 
 
 (*The set of all reachable states is Always*)
@@ -312,8 +310,7 @@
 apply (blast intro: constrains_imp_Constrains)
 done
 
-lemmas Always_reachable =
-    invariant_reachable [THEN invariant_imp_Always, standard]
+lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
 
 lemma Always_eq_invariant_reachable:
      "Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
@@ -355,10 +352,10 @@
               Constrains_eq_constrains Int_assoc [symmetric])
 
 (* [| F \<in> Always INV;  F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
-lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
+lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1]
 
 (* [| F \<in> Always INV;  F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
-lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
+lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
 
 (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
 lemma Always_Constrains_weaken:
@@ -390,7 +387,7 @@
 
 (*Delete the nearest invariance assumption (which will be the second one
   used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
+lemmas Always_thin = thin_rl [of "F \<in> Always A"]
 
 
 subsection{*Totalize*}
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/ELT.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -418,7 +418,7 @@
 apply (blast intro: subset_imp_leadsETo)
 done
 
-lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
+lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
 
 lemma LeadsETo_weaken_R [rule_format]:
      "[| F : A LeadsTo[CC] A';  A' <= B' |] ==> F : A LeadsTo[CC] B'"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Rename.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -140,7 +140,7 @@
 lemma bij_rename: "bij h ==> bij (rename h)"
 apply (simp (no_asm_simp) add: rename_def bij_extend)
 done
-lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]
+lemmas surj_rename = bij_rename [THEN bij_is_surj]
 
 lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
 apply (unfold inj_on_def, auto)
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -69,8 +69,8 @@
     MA7:  "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
 
 
-lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard]
-lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard]
+lemmas E_imp_in_V_L = Graph2 [THEN conjunct1]
+lemmas E_imp_in_V_R = Graph2 [THEN conjunct2]
 
 lemma lemma2:
      "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -42,10 +42,10 @@
               Int_assoc [symmetric])
 
 (* [| F \<in> Always C;  F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
-lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
+lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1]
 
 (* [| F \<in> Always INV;  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
-lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
+lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2]
 
 
 subsection{*Introduction rules: Basis, Trans, Union*}
@@ -104,7 +104,7 @@
 apply (blast intro: subset_imp_leadsTo)
 done
 
-lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
+lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, simp]
 
 lemma LeadsTo_weaken_R:
      "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -274,7 +274,7 @@
 by (unfold stable_def constrains_def, blast)
 
 (*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
-lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard]
+lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]
 
 
 subsubsection{*invariant*}
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Union.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -332,7 +332,7 @@
 lemma ok_commute: "(F ok G) = (G ok F)"
 by (auto simp add: ok_def)
 
-lemmas ok_sym = ok_commute [THEN iffD1, standard]
+lemmas ok_sym = ok_commute [THEN iffD1]
 
 lemma ok_iff_OK:
      "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/WFair.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -235,13 +235,13 @@
 lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B"
 by (unfold ensures_def constrains_def transient_def, blast)
 
-lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
+lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
 
-lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]
+lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo]
 
-lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]
+lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, simp]
 
-lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]
+lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, simp]
 
 
 
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -45,7 +45,7 @@
       \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
 
 lemmas fine_induct [induct set: fine] =
-  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
+  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P
 
 lemma fine_single:
   "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/ex/Tree23.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -330,12 +330,13 @@
 "dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
 
 lemmas dfull_case_intros =
-  ord.exhaust [where y=y and P="dfull a (ord_case b c d y)", standard]
-  option.exhaust [where y=y and P="dfull a (option_case b c y)", standard]
-  prod.exhaust [where y=y and P="dfull a (prod_case b y)", standard]
-  bool.exhaust [where y=y and P="dfull a (bool_case b c y)", standard]
-  tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))", standard]
-  tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
+  ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"]
+  option.exhaust [where y=y and P="dfull a (option_case b c y)"]
+  prod.exhaust [where y=y and P="dfull a (prod_case b y)"]
+  bool.exhaust [where y=y and P="dfull a (bool_case b c y)"]
+  tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"]
+  tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"]
+  for a b c d e y
 
 lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
 proof -