src/HOLCF/Holcfb.thy

--- a/src/HOLCF/Holcfb.thy	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Holcfb.thy	Thu Jun 29 16:28:40 1995 +0200
@@ -13,9 +13,9 @@
 
 theleast     :: "(nat=>bool)=>nat"
 
-rules
+defs
 
-theleast_def    "theleast(P) == (@z.(P(z) & (!n.P(n)-->z<=n)))"
+theleast_def    "theleast P == (@z.(P z & (!n.P n --> z<=n)))"
 
 end