1.1 --- a/src/HOL/UNITY/Constrains.ML	Fri Aug 14 12:03:01 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.ML	Fri Aug 14 12:06:34 1998 +0200
     1.3 @@ -7,18 +7,6 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -
     1.8 -(**MOVE TO EQUALITIES.ML**)
     1.9 -
    1.10 -Goal "(A Un B <= C) = (A <= C & B <= C)";
    1.11 -by (Blast_tac 1);
    1.12 -qed "Un_subset_iff";
    1.13 -
    1.14 -Goal "(C <= A Int B) = (C <= A & C <= B)";
    1.15 -by (Blast_tac 1);
    1.16 -qed "Int_subset_iff";
    1.17 -
    1.18 -
    1.19  (*** Constrains ***)
    1.20  
    1.21  (*constrains (Acts prg) B B'
    1.22 @@ -255,7 +243,7 @@
    1.23                          assume_tac THEN'
    1.24  			etac Invariant_thin;
    1.25  
    1.26 -(*Combines two invariance THEOREMS into one.*)
    1.27 +(*Combines a list of invariance THEOREMS into one.*)
    1.28  val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
    1.29  
    1.30  

     2.1 --- a/src/HOL/equalities.ML	Fri Aug 14 12:03:01 1998 +0200
     2.2 +++ b/src/HOL/equalities.ML	Fri Aug 14 12:06:34 1998 +0200
     2.3 @@ -124,7 +124,7 @@
     2.4  AddIffs [image_is_empty];
     2.5  
     2.6  Goal "f `` {x. P x} = {f x | x. P x}";
     2.7 -by(Blast_tac 1);
     2.8 +by (Blast_tac 1);
     2.9  qed "image_Collect";
    2.10  Addsimps [image_Collect];
    2.11  
    2.12 @@ -217,6 +217,11 @@
    2.13  qed "Int_UNIV";
    2.14  Addsimps[Int_UNIV];
    2.15  
    2.16 +Goal "(C <= A Int B) = (C <= A & C <= B)";
    2.17 +by (Blast_tac 1);
    2.18 +qed "Int_subset_iff";
    2.19 +
    2.20 +
    2.21  section "Un";
    2.22  
    2.23  Goal "A Un A = A";
    2.24 @@ -322,6 +327,11 @@
    2.25  qed "Un_empty";
    2.26  Addsimps[Un_empty];
    2.27  
    2.28 +Goal "(A Un B <= C) = (A <= C & B <= C)";
    2.29 +by (Blast_tac 1);
    2.30 +qed "Un_subset_iff";
    2.31 +
    2.32 +
    2.33  section "Compl";
    2.34  
    2.35  Goal "A Int Compl(A) = {}";