changeset 62390 | 842917225d56 |
parent 61956 | 38b73f7940af |
child 67613 | ce654b0e6d69 |
--- a/src/HOL/Auth/Guard/Guard.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Auth/Guard/Guard.thy Tue Feb 23 16:25:08 2016 +0100 @@ -304,4 +304,4 @@ apply (drule_tac G="G Un (H Int keysfor G)" in Guard_invKey_finite) by (auto simp: Guard_def intro: analz_sub) -end \ No newline at end of file +end