generalized UNION1 to UNION

--- a/src/HOL/Auth/Message.ML	Wed Nov 05 13:27:29 1997 +0100
+++ b/src/HOL/Auth/Message.ML	Wed Nov 05 13:27:58 1997 +0100
@@ -47,9 +47,9 @@
 by (Blast_tac 1);
 qed "keysFor_Un";
 
-goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
+goalw thy [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
 by (Blast_tac 1);
-qed "keysFor_UN1";
+qed "keysFor_UN";
 
 (*Monotonicity*)
 goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
@@ -85,12 +85,12 @@
 by (Auto_tac());
 qed "keysFor_insert_Crypt";
 
-Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, 
+Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
           keysFor_insert_Agent, keysFor_insert_Nonce, 
 	  keysFor_insert_Number, keysFor_insert_Key, 
           keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
 AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
-	keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E];
+	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
 
 goalw thy [keysFor_def] "keysFor (Key``E) = {}";
 by (Auto_tac ());
@@ -195,16 +195,11 @@
 by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
 qed "parts_UN";
 
-goal thy "parts(UN x. H x) = (UN x. parts(H x))";
-by (simp_tac (simpset() addsimps [UNION1_def, parts_UN]) 1);
-qed "parts_UN1";
-
 (*Added to simplify arguments to parts, analz and synth.
   NOTE: the UN versions are no longer used!*)
-Addsimps [parts_Un, parts_UN, parts_UN1];
+Addsimps [parts_Un, parts_UN];
 AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
-	parts_UN RS equalityD1 RS subsetD RS UN_E,
-	parts_UN1 RS equalityD1 RS subsetD RS UN1_E];
+	parts_UN RS equalityD1 RS subsetD RS UN_E];
 
 goal thy "insert X (parts H) <= parts(insert X H)";
 by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
@@ -559,13 +554,13 @@
 by (ALLGOALS Blast_tac);
 qed "analz_trivial";
 
-(*Helps to prove Fake cases*)
-goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)";
+(*These two are obsolete (with a single Spy) but cost little to prove...*)
+goal thy "!!X. X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
 by (etac analz.induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
 val lemma = result();
 
-goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)";
+goal thy "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
 by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
 qed "analz_UN_analz";
 Addsimps [analz_UN_analz];