# HG changeset patch
# User nipkow
# Date 964633339 -7200
# Node ID e5180c86977295830f9ed83e56617710fa47ec1a
# Parent  7bc054e9fb1c8ecef3a937262675f29c21fb1800
*** empty log message ***

diff -r 7bc054e9fb1c -r e5180c869772 src/HOL/Main.thy
--- 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*)
diff -r 7bc054e9fb1c -r e5180c869772 src/HOL/equalities.ML
--- 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";