new default simprule Collect_const and new them Diff_insert_absorb

--- a/src/HOL/equalities.ML	Mon Oct 11 10:50:41 1999 +0200
+++ b/src/HOL/equalities.ML	Mon Oct 11 10:51:24 1999 +0200
@@ -12,10 +12,11 @@
 
 section "{}";
 
-Goal "{x. False} = {}";
-by (Blast_tac 1);
-qed "Collect_False_empty";
-Addsimps [Collect_False_empty];
+(*supersedes Collect_False_empty*)
+Goal "{s. P} = (if P then UNIV else {})";
+by (Force_tac 1);
+qed "Collect_const";
+Addsimps [Collect_const];
 
 Goal "(A <= {}) = (A = {})";
 by (Blast_tac 1);
@@ -675,6 +676,10 @@
 by (Blast_tac 1);
 qed "insert_Diff";
 
+Goal "x ~: A ==> (insert x A) - {x} = A";
+by Auto_tac;
+qed "Diff_insert_absorb";
+
 Goal "A Int (B-A) = {}";
 by (Blast_tac 1);
 qed "Diff_disjoint";