src/HOL/Auth/Event.thy

 lemmas analz_mono_contra =
        knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
        knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
        knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
 
-ML
-{*
-val analz_mono_contra_tac = 
-  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
-  in
-    rtac analz_impI THEN' 
-    REPEAT1 o 
-      (dresolve_tac (thms"analz_mono_contra"))
-    THEN' mp_tac
-  end
-*}
-
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
 by (induct e, auto simp: knows_Cons)
 
 lemma initState_subset_knows: "initState A \<subseteq> knows A evs"

 by (force 
     dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
            analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
 
+
+ML
+{*
+val analz_mono_contra_tac = 
+  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
+  in
+    rtac analz_impI THEN' 
+    REPEAT1 o 
+      (dresolve_tac @{thms analz_mono_contra})
+    THEN' mp_tac
+  end
+*}
+
 method_setup analz_mono_contra = {*
     Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
 
 ML
 {*
-val knows_Cons     = thm "knows_Cons"
-val used_Nil       = thm "used_Nil"
-val used_Cons      = thm "used_Cons"
-
-val Notes_imp_used = thm "Notes_imp_used";
-val Says_imp_used = thm "Says_imp_used";
-val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
-val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
-val knows_Spy_partsEs = thms "knows_Spy_partsEs";
-val spies_partsEs = thms "spies_partsEs";
-val Says_imp_spies = thm "Says_imp_spies";
-val parts_insert_spies = thm "parts_insert_spies";
-val Says_imp_knows = thm "Says_imp_knows";
-val Notes_imp_knows = thm "Notes_imp_knows";
-val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
-val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
-val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
-val usedI = thm "usedI";
-val initState_into_used = thm "initState_into_used";
-val used_Says = thm "used_Says";
-val used_Notes = thm "used_Notes";
-val used_Gets = thm "used_Gets";
-val used_nil_subset = thm "used_nil_subset";
-val analz_mono_contra = thms "analz_mono_contra";
-val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
-val initState_subset_knows = thm "initState_subset_knows";
-val keysFor_parts_insert = thm "keysFor_parts_insert";
-
-
-val synth_analz_mono = thm "synth_analz_mono";
-
-val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
-val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
-val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
-
-
 val synth_analz_mono_contra_tac = 
   let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   in
     rtac syan_impI THEN' 
     REPEAT1 o 
       (dresolve_tac 
-       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
-        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
-	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
+       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
+       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
+       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
     THEN'
     mp_tac
   end;
 *}