# HG changeset patch
# User paulson
# Date 888574078 -3600
# Node ID 73ba4d19f80246cb093cc8942b4da5dbcfbb7fc0
# Parent  e3fbcab526a2c0f1da971a19410ae5a606b674f3
New absorbsion laws, etc

diff -r e3fbcab526a2 -r 73ba4d19f802 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Feb 27 11:07:13 1998 +0100
+++ b/src/HOL/equalities.ML	Fri Feb 27 11:07:58 1998 +0100
@@ -152,6 +152,14 @@
 (*Intersection is an AC-operator*)
 val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
 
+goal thy "!!A B. B<=A ==> A Int B = B";
+by (Blast_tac 1);
+qed "Int_absorb1";
+
+goal thy "!!A B. A<=B ==> A Int B = A";
+by (Blast_tac 1);
+qed "Int_absorb2";
+
 goal thy "{} Int B = {}";
 by (Blast_tac 1);
 qed "Int_empty_left";
@@ -223,6 +231,14 @@
 (*Union is an AC-operator*)
 val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
 
+goal thy "!!A B. A<=B ==> A Un B = B";
+by (Blast_tac 1);
+qed "Un_absorb1";
+
+goal thy "!!A B. B<=A ==> A Un B = A";
+by (Blast_tac 1);
+qed "Un_absorb2";
+
 goal thy "{} Un B = B";
 by (Blast_tac 1);
 qed "Un_empty_left";
@@ -550,7 +566,7 @@
 
 goal thy "A-B = A Int Compl B";
 by (Blast_tac 1);
-qed "Diff_eq_Int_Compl";
+qed "Diff_eq";
 
 goal thy "A-A = {}";
 by (Blast_tac 1);
@@ -636,7 +652,7 @@
 by (Blast_tac 1);
 qed "Un_Diff";
 
-goal thy "(A Int B) - C = (A - C) Int (B - C)";
+goal thy "(A Int B) - C = A Int (B - C)";
 by (Blast_tac 1);
 qed "Int_Diff";