new theorem Fake_parts_insert_in_Un
authorpaulson
Mon Apr 09 14:49:51 2001 +0200 (2001-04-09)
changeset 112453d9d25a3375b
parent 11244 ca1de97d67c8
child 11246 64d0bcccb03a
new theorem Fake_parts_insert_in_Un
src/HOL/Auth/Message.thy
     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"