diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Set.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -50,17 +50,17 @@
 
 
 rules
-  mem_Collect_iff       "(a : {x.P(x)}) <-> P(a)"
-  set_extension         "A=B <-> (ALL x.x:A <-> x:B)"
+  mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"
+  set_extension         "A=B <-> (ALL x. x:A <-> x:B)"
 
   Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
   Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
   mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
   subset_def    "A <= B      == ALL x:A. x:B"
-  singleton_def "{a}         == {x.x=a}"
-  empty_def     "{}          == {x.False}"
-  Un_def        "A Un B      == {x.x:A | x:B}"
-  Int_def       "A Int B     == {x.x:A & x:B}"
+  singleton_def "{a}         == {x. x=a}"
+  empty_def     "{}          == {x. False}"
+  Un_def        "A Un B      == {x. x:A | x:B}"
+  Int_def       "A Int B     == {x. x:A & x:B}"
   Compl_def     "Compl(A)    == {x. ~x:A}"
   INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
   UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"