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