# HG changeset patch
# User wenzelm
# Date 1087828758 -7200
# Node ID 2b5e9b80a8e5fe695c5a1f5b46746a76af71538e
# Parent  ff1c919f49829e324e294b81ea8dde87ccf76c79
avoid \...\;

diff -r ff1c919f4982 -r 2b5e9b80a8e5 src/HOL/Auth/Shared.thy
--- 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"