src/HOL/Auth/Event.thy
changeset 45605 a89b4bc311a5
parent 41693 47532fe9e075
child 46471 2289a3869c88
     1.1 --- a/src/HOL/Auth/Event.thy	Sun Nov 20 20:59:30 2011 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Sun Nov 20 21:05:23 2011 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4  (*Simplifying   
     1.5   parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
     1.6    This version won't loop with the simplifier.*)
     1.7 -lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
     1.8 +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
     1.9  
    1.10  lemma knows_Spy_Says [simp]:
    1.11       "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
    1.12 @@ -138,10 +138,10 @@
    1.13  text{*Elimination rules: derive contradictions from old Says events containing
    1.14    items known to be fresh*}
    1.15  lemmas Says_imp_parts_knows_Spy = 
    1.16 -       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
    1.17 +       Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl] 
    1.18  
    1.19  lemmas knows_Spy_partsEs =
    1.20 -     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
    1.21 +     Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl]
    1.22  
    1.23  lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
    1.24  
    1.25 @@ -278,7 +278,7 @@
    1.26      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
    1.27  
    1.28  
    1.29 -lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
    1.30 +lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
    1.31  
    1.32  ML
    1.33  {*
    1.34 @@ -294,7 +294,7 @@
    1.35  
    1.36  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.37  
    1.38 -lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
    1.39 +lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
    1.40  
    1.41  ML
    1.42  {*