src/HOL/Auth/Shared.thy
changeset 13507 febb8e5d2a9d
parent 12415 74977582a585
child 13907 2bc462b99e70
     1.1 --- a/src/HOL/Auth/Shared.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4  (*Lets blast_tac perform this step without needing the simplifier*)
     1.5  lemma invKey_shrK_iff [iff]:
     1.6       "(Key (invKey K) \<in> X) = (Key K \<in> X)"
     1.7 -by auto;
     1.8 +by auto
     1.9  
    1.10  (*Specialized methods*)
    1.11