src/HOL/Auth/Message.thy
changeset 11245 3d9d25a3375b
parent 11230 756c5034f08b
child 11251 a6816d47f41d
     1.1 --- a/src/HOL/Auth/Message.thy	Mon Apr 09 10:12:33 2001 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Mon Apr 09 14:49:51 2001 +0200
     1.3 @@ -135,6 +135,11 @@
     1.4  
     1.5  use "Message_lemmas.ML"
     1.6  
     1.7 +lemma Fake_parts_insert_in_Un:
     1.8 +     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
     1.9 +      ==> Z \<in>  synth (analz H) \<union> parts H";
    1.10 +by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
    1.11 +
    1.12  method_setup spy_analz = {*
    1.13      Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
    1.14      "for proving the Fake case when analz is involved"