# HG changeset patch
# User paulson
# Date 826549790 -3600
# Node ID 822575c737bd96dd78d7bb318f2419fe465026d9
# Parent  717f8816eca5d9250ea2a039a2d4d92473a9d918
Deleted faulty comment; proved new rule Inter_Un_subset

diff -r 717f8816eca5 -r 822575c737bd src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Mar 11 14:08:09 1996 +0100
+++ b/src/HOL/equalities.ML	Mon Mar 11 14:09:50 1996 +0100
@@ -277,12 +277,9 @@
 qed "Inter_insert";
 Addsimps[Inter_insert];
 
-(* Why does fast_tac fail???
-goal Set.thy "Inter(A Int B) = Inter(A) Int Inter(B)";
-by (fast_tac eq_cs 1);
-qed "Inter_Int_distrib";
-Addsimps[Inter_Int_distrib];
-*)
+goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
+by (fast_tac set_cs 1);
+qed "Inter_Un_subset";
 
 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
 by (best_tac eq_cs 1);