# 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";