src/HOL/Auth/Event.thy
changeset 41693 47532fe9e075
parent 38964 b1a7bef0907a
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Feb 02 15:47:57 2011 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Feb 02 14:11:26 2011 +0000
     1.3 @@ -271,7 +271,7 @@
     1.4  text{*For proving @{text new_keys_not_used}*}
     1.5  lemma keysFor_parts_insert:
     1.6       "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
     1.7 -      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
     1.8 +      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"
     1.9  by (force 
    1.10      dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
    1.11             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]