# HG changeset patch
# User paulson
# Date 986820591 -7200
# Node ID 3d9d25a3375bc7d7c261b239cf863d46c10054bd
# Parent  ca1de97d67c86d2d898350f0946272d6008bdad8
new theorem Fake_parts_insert_in_Un

diff -r ca1de97d67c8 -r 3d9d25a3375b src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Apr 09 10:12:33 2001 +0200
+++ b/src/HOL/Auth/Message.thy	Mon Apr 09 14:49:51 2001 +0200
@@ -135,6 +135,11 @@
 
 use "Message_lemmas.ML"
 
+lemma Fake_parts_insert_in_Un:
+     "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
+      ==> Z \<in>  synth (analz H) \<union> parts H";
+by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
+
 method_setup spy_analz = {*
     Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
     "for proving the Fake case when analz is involved"