--- 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)