--- a/src/HOL/Main.thy Tue Jul 25 23:33:13 2000 +0200
+++ b/src/HOL/Main.thy Wed Jul 26 19:42:19 2000 +0200
@@ -1,1 +1,1 @@
-Main = Map + String (*theory Main includes everything*)
+Main = While + Map + String (*theory Main includes everything*)
--- a/src/HOL/equalities.ML Tue Jul 25 23:33:13 2000 +0200
+++ b/src/HOL/equalities.ML Wed Jul 26 19:42:19 2000 +0200
@@ -425,6 +425,16 @@
Addsimps [Compl_UNIV_eq, Compl_empty_eq];
+Goal "(-A <= -B) = (B <= (A::'a set))";
+by(Blast_tac 1);
+qed "Compl_subset_Compl_iff";
+AddIffs [Compl_subset_Compl_iff];
+
+Goal "(-A = -B) = (A = (B::'a set))";
+by(Blast_tac 1);
+qed "Compl_eq_Compl_iff";
+AddIffs [Compl_eq_Compl_iff];
+
section "Union";