src/CCL/equalities.ML

--- a/src/CCL/equalities.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/equalities.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -64,11 +64,11 @@
 
 (** Simple properties of Compl -- complement of a set **)
 
-goal Set.thy "A Int Compl(A) = {x.False}";
+goal Set.thy "A Int Compl(A) = {x. False}";
 by (fast_tac eq_cs 1);
 qed "Compl_disjoint";
 
-goal Set.thy "A Un Compl(A) = {x.True}";
+goal Set.thy "A Un Compl(A) = {x. True}";
 by (fast_tac eq_cs 1);
 qed "Compl_partition";
 
@@ -106,7 +106,7 @@
 qed "Union_Un_distrib";
 
 val prems = goal Set.thy
-   "(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
+   "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "Union_disjoint";