tidying
authorpaulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 60190e55c2fb2ebb
parent 6018 8131f37f4ba3
child 6020 4b109bf75976
tidying
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Union.ML	Mon Dec 07 18:23:39 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Union.ML	Mon Dec 07 18:26:25 1998 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5  (** JN **)
     1.6  
     1.7 -Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = (SKIP UNIV)";
     1.8 +Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP UNIV";
     1.9  by Auto_tac;
    1.10  qed "JN_empty";
    1.11  Addsimps [JN_empty];
    1.12 @@ -76,8 +76,9 @@
    1.13  	      simpset() addsimps [JOIN_def]));
    1.14  qed "Init_JN";
    1.15  
    1.16 +(*If I={} then the LHS is (SKIP UNIV) while the RHS is {}.*)
    1.17  Goalw [eqStates_def]
    1.18 -     "[| i: I;  eqStates I F |] ==> Acts (JN i:I. F i) = (UN i:I. Acts (F i))";
    1.19 +     "[| eqStates I F; i: I |] ==> Acts (JN i:I. F i) = (UN i:I. Acts (F i))";
    1.20  by (Clarify_tac 1);
    1.21  by (subgoal_tac "(UN i:I. Acts (F i)) <= Pow (St Times St)" 1);
    1.22  by (blast_tac (claset() addEs [equalityE]