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