--- a/src/HOLCF/Pcpo.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Pcpo.thy Fri Oct 10 19:02:28 1997 +0200
@@ -17,7 +17,7 @@
(* ****************************** *)
axclass pcpo < cpo
- least "? x.!y.x<<y"
+ least "? x.!y. x<<y"
consts
UU :: "'a::pcpo"
@@ -26,16 +26,16 @@
UU :: "'a::pcpo" ("\\<bottom>")
defs
- UU_def "UU == @x.!y.x<<y"
+ UU_def "UU == @x.!y. x<<y"
(* further useful classes for HOLCF domains *)
axclass chfin<cpo
-chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
+chfin "!Y. is_chain Y-->(? n. max_in_chain n Y)"
axclass flat<pcpo
-ax_flat "! x y.x << y --> (x = UU) | (x=y)"
+ax_flat "! x y. x << y --> (x = UU) | (x=y)"
end