# HG changeset patch
# User paulson
# Date 842613348 -7200
# Node ID 4ddfafdeefa4b2f0adef3d7302232d479586023a
# Parent  77e7ef8e5c3b20f14d244a03f5a2a14e8b7b7af4
Removal of obsolete thm Fake_parts_insert

diff -r 77e7ef8e5c3b -r 4ddfafdeefa4 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Sep 13 13:15:00 1996 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Sep 13 13:15:48 1996 +0200
@@ -616,15 +616,6 @@
 by (Fast_tac 1);
 qed "parts_insert_subset_Un";
 
-(*More specifically for Fake****OBSOLETE VERSION
-goal thy "!!H. X: synth (analz H) ==> \
-\              parts (insert X H) <= synth (analz H) Un parts H";
-bd parts_insert_subset_Un 1;
-by (Full_simp_tac 1);
-by (Fast_tac 1);
-qed "Fake_parts_insert";
-*)
-
 (*More specifically for Fake*)
 goal thy "!!H. X: synth (analz G) ==> \
 \              parts (insert X H) <= synth (analz G) Un parts G Un parts H";