# HG changeset patch
# User paulson
# Date 846504085 -3600
# Node ID aeba09ebd8bcad993369a47fe331f81d9221dcd8
# Parent  3106a99d30a515b9705ec0310d2a22281d807765
Tidied up a big mess in UN_parts_sees_Says

diff -r 3106a99d30a5 -r aeba09ebd8bc src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Mon Oct 28 12:55:24 1996 +0100
+++ b/src/HOL/Auth/Shared.ML	Mon Oct 28 13:01:25 1996 +0100
@@ -154,14 +154,15 @@
 by (Fast_tac 1);
 qed "sees_subset_sees_Says";
 
-(*Pushing Unions into parts; one of the A's equals B, and thus sees lost Y*)
+(*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
+  Used to prove new_keys_not_seen.*)
 goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
 \         parts {Y} Un (UN A. parts (sees lost A evs))";
 by (Step_tac 1);
-by (etac rev_mp 1);     (*for some reason, split_tac does not work on assumptions*)
-val ss = (!simpset addsimps [parts_Un, sees_Cons] 
-                   setloop split_tac [expand_if]);
-by (ALLGOALS (fast_tac (!claset addss ss)));
+by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
+by (ALLGOALS
+    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
+                       setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Says";
 
 goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";