changeset 59807 | 22bc39064290 |
parent 58889 | 5b7a9633cfa8 |
child 61830 | 4f5ab843cf5b |
--- a/src/HOL/Auth/Yahalom.thy Wed Mar 25 10:41:53 2015 +0100 +++ b/src/HOL/Auth/Yahalom.thy Wed Mar 25 10:44:57 2015 +0100 @@ -403,7 +403,7 @@ txt{*YM3*} apply blast txt{*YM4*} -apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify) +apply (erule_tac V = "\<forall>KK. P KK" for P in thin_rl, clarify) txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}. Previous two steps make the next step faster.*}