diff -r acc18a5d2b1a -r febb8e5d2a9d src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Shared.thy	Sat Aug 17 14:55:08 2002 +0200
@@ -39,7 +39,7 @@
 (*Lets blast_tac perform this step without needing the simplifier*)
 lemma invKey_shrK_iff [iff]:
      "(Key (invKey K) \<in> X) = (Key K \<in> X)"
-by auto;
+by auto
 
 (*Specialized methods*)