subset_empty is no longer a simprule
authorpaulson
Fri Jun 16 13:18:55 2000 +0200 (2000-06-16)
changeset 90775bf9b0d6df8a
parent 9076 108ec332625d
child 9078 b8780970d0ed
subset_empty is no longer a simprule
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Fri Jun 16 13:16:07 2000 +0200
     1.2 +++ b/src/HOL/equalities.ML	Fri Jun 16 13:18:55 2000 +0200
     1.3 @@ -18,10 +18,11 @@
     1.4  qed "Collect_const";
     1.5  Addsimps [Collect_const];
     1.6  
     1.7 +(*If added as a simprule it can cause looping when equalityE is also present:
     1.8 +  A={} goes to {}<=A and A<={} and then back to A={} !*)
     1.9  Goal "(A <= {}) = (A = {})";
    1.10  by (Blast_tac 1);
    1.11  qed "subset_empty";
    1.12 -Addsimps [subset_empty];
    1.13  
    1.14  Goalw [psubset_def] "~ (A < {})";
    1.15  by (Blast_tac 1);