| changeset 4422 | 21238c9d363e |
| parent 4091 | 771b1f6422a8 |
| child 4449 | df30e75f670f |
--- a/src/HOL/Auth/Recur.ML Tue Dec 16 15:15:38 1997 +0100 +++ b/src/HOL/Auth/Recur.ML Tue Dec 16 15:17:26 1997 +0100 @@ -247,8 +247,6 @@ by (ALLGOALS (asm_simp_tac (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); -(*Base*) -by (Blast_tac 1); (*Fake*) by (spy_analz_tac 1); val raw_analz_image_freshK = result();