| changeset 3451 | d10f100676d8 |
| parent 3207 | fe79ad367d77 |
| child 3465 | e85c24717cad |
--- a/src/HOL/Auth/Recur.ML Thu Jun 19 11:28:55 1997 +0200 +++ b/src/HOL/Auth/Recur.ML Thu Jun 19 11:31:14 1997 +0200 @@ -268,8 +268,8 @@ (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); (*Base*) by (Blast_tac 1); -(*RA4, RA2, Fake*) -by (REPEAT (spy_analz_tac 1)); +(*Fake*) +by (spy_analz_tac 1); val raw_analz_image_freshK = result(); qed_spec_mp "analz_image_freshK";