src/HOL/Auth/OtwayRees.ML
changeset 4422 21238c9d363e
parent 4091 771b1f6422a8
child 4449 df30e75f670f
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Dec 16 15:15:38 1997 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Dec 16 15:17:26 1997 +0100
     1.3 @@ -173,9 +173,7 @@
     1.4  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     1.5  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     1.6  (*Fake*) 
     1.7 -by (spy_analz_tac 2);
     1.8 -(*Base*)
     1.9 -by (Blast_tac 1);
    1.10 +by (spy_analz_tac 1);
    1.11  qed_spec_mp "analz_image_freshK";
    1.12  
    1.13