# HG changeset patch
# User paulson
# Date 903089194 -7200
# Node ID 7356d0c88b1b394737c843e3670dc86a029fe861
# Parent  72bf8039b53f3a42249f77af9c0b63f7b232b73e
Moved Un_subset_iff and Int_subset_iff from UNITY to equalities.ML

diff -r 72bf8039b53f -r 7356d0c88b1b src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Fri Aug 14 12:03:01 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Fri Aug 14 12:06:34 1998 +0200
@@ -7,18 +7,6 @@
 *)
 
 
-
-(**MOVE TO EQUALITIES.ML**)
-
-Goal "(A Un B <= C) = (A <= C & B <= C)";
-by (Blast_tac 1);
-qed "Un_subset_iff";
-
-Goal "(C <= A Int B) = (C <= A & C <= B)";
-by (Blast_tac 1);
-qed "Int_subset_iff";
-
-
 (*** Constrains ***)
 
 (*constrains (Acts prg) B B'
@@ -255,7 +243,7 @@
                         assume_tac THEN'
 			etac Invariant_thin;
 
-(*Combines two invariance THEOREMS into one.*)
+(*Combines a list of invariance THEOREMS into one.*)
 val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
 
 
diff -r 72bf8039b53f -r 7356d0c88b1b src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Aug 14 12:03:01 1998 +0200
+++ b/src/HOL/equalities.ML	Fri Aug 14 12:06:34 1998 +0200
@@ -124,7 +124,7 @@
 AddIffs [image_is_empty];
 
 Goal "f `` {x. P x} = {f x | x. P x}";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "image_Collect";
 Addsimps [image_Collect];
 
@@ -217,6 +217,11 @@
 qed "Int_UNIV";
 Addsimps[Int_UNIV];
 
+Goal "(C <= A Int B) = (C <= A & C <= B)";
+by (Blast_tac 1);
+qed "Int_subset_iff";
+
+
 section "Un";
 
 Goal "A Un A = A";
@@ -322,6 +327,11 @@
 qed "Un_empty";
 Addsimps[Un_empty];
 
+Goal "(A Un B <= C) = (A <= C & B <= C)";
+by (Blast_tac 1);
+qed "Un_subset_iff";
+
+
 section "Compl";
 
 Goal "A Int Compl(A) = {}";