src/HOL/Auth/Message.thy
changeset 11251 a6816d47f41d
parent 11245 3d9d25a3375b
child 11264 a47a9288f3f6
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Apr 11 11:53:54 2001 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Apr 12 12:45:05 2001 +0200
     1.3 @@ -135,6 +135,8 @@
     1.4  
     1.5  use "Message_lemmas.ML"
     1.6  
     1.7 +lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
     1.8 +
     1.9  lemma Fake_parts_insert_in_Un:
    1.10       "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
    1.11        ==> Z \<in>  synth (analz H) \<union> parts H";