# HG changeset patch
# User paulson
# Date 961154335 -7200
# Node ID 5bf9b0d6df8ac99a7a2de92e2ba17621e7c96a31
# Parent  108ec332625d2d9c21ea5866c0dd955b8a0a77dc
subset_empty is no longer a simprule

diff -r 108ec332625d -r 5bf9b0d6df8a src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jun 16 13:16:07 2000 +0200
+++ b/src/HOL/equalities.ML	Fri Jun 16 13:18:55 2000 +0200
@@ -18,10 +18,11 @@
 qed "Collect_const";
 Addsimps [Collect_const];
 
+(*If added as a simprule it can cause looping when equalityE is also present:
+  A={} goes to {}<=A and A<={} and then back to A={} !*)
 Goal "(A <= {}) = (A = {})";
 by (Blast_tac 1);
 qed "subset_empty";
-Addsimps [subset_empty];
 
 Goalw [psubset_def] "~ (A < {})";
 by (Blast_tac 1);