--- 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
{*