diff -r 542f0563d7b4 -r 133e4a6474e3 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Mon Sep 21 14:22:32 2009 +0200
+++ b/src/HOL/Auth/Public.thy	Mon Sep 21 15:33:39 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Auth/Public
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
@@ -8,7 +7,9 @@
 Private and public keys; initial states of agents
 *)
 
-theory Public imports Event begin
+theory Public
+imports Event
+begin
 
 lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
 by (simp add: symKeys_def)