| changeset 4422 | 21238c9d363e |
| parent 4155 | 53f60f51333c |
| child 4449 | df30e75f670f |
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 16 15:15:38 1997 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 16 15:17:26 1997 +0100 @@ -165,9 +165,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";