--- a/src/HOL/Auth/Shared.thy Mon Jun 21 16:39:09 2004 +0200
+++ b/src/HOL/Auth/Shared.thy Mon Jun 21 16:39:18 2004 +0200
@@ -63,8 +63,8 @@
(*Specialized to shared-key model: no @{term invKey}*)
lemma keysFor_parts_insert:
- "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] \
-\ ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+ "[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |]
+ ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
by (force dest: Event.keysFor_parts_insert)
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"