# HG changeset patch
# User paulson
# Date 913051585 -3600
# Node ID 0e55c2fb2ebb726cc24a15e44098a1f09ccb7218
# Parent  8131f37f4ba36dfe884c4c5dc0ff1e68e62b7478
tidying

diff -r 8131f37f4ba3 -r 0e55c2fb2ebb src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Mon Dec 07 18:23:39 1998 +0100
+++ b/src/HOL/UNITY/Union.ML	Mon Dec 07 18:26:25 1998 +0100
@@ -62,7 +62,7 @@
 
 (** JN **)
 
-Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = (SKIP UNIV)";
+Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP UNIV";
 by Auto_tac;
 qed "JN_empty";
 Addsimps [JN_empty];
@@ -76,8 +76,9 @@
 	      simpset() addsimps [JOIN_def]));
 qed "Init_JN";
 
+(*If I={} then the LHS is (SKIP UNIV) while the RHS is {}.*)
 Goalw [eqStates_def]
-     "[| i: I;  eqStates I F |] ==> Acts (JN i:I. F i) = (UN i:I. Acts (F i))";
+     "[| eqStates I F; i: I |] ==> Acts (JN i:I. F i) = (UN i:I. Acts (F i))";
 by (Clarify_tac 1);
 by (subgoal_tac "(UN i:I. Acts (F i)) <= Pow (St Times St)" 1);
 by (blast_tac (claset() addEs [equalityE]