src/HOLCF/Cprod1.thy

--- a/src/HOLCF/Cprod1.thy	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Cprod1.thy	Thu Jun 29 16:28:40 1995 +0200
@@ -14,9 +14,9 @@
 consts
   less_cprod	:: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool"	
 
-rules
+defs
 
-  less_cprod_def "less_cprod(p1,p2) == ( fst(p1) << fst(p2) &
+  less_cprod_def "less_cprod p1 p2 == ( fst(p1) << fst(p2) &
 					snd(p1) << snd(p2))"
 
 end