changeset 9338 | fcf7f29a3447 |
parent 9312 | a93a7b6bb654 |
child 9399 | effc8d44c89c |
--- a/src/HOL/equalities.ML Fri Jul 14 14:51:02 2000 +0200 +++ b/src/HOL/equalities.ML Fri Jul 14 16:27:37 2000 +0200 @@ -18,11 +18,10 @@ 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);