--- a/src/HOLCF/ex/Loop.thy Fri Jun 02 18:24:48 2006 +0200
+++ b/src/HOLCF/ex/Loop.thy Fri Jun 02 19:41:37 2006 +0200
@@ -9,13 +9,12 @@
imports HOLCF
begin
-constdefs
+definition
step :: "('a -> tr)->('a -> 'a)->'a->'a"
- "step == (LAM b g x. If b$x then g$x else x fi)"
+ "step = (LAM b g x. If b$x then g$x else x fi)"
while :: "('a -> tr)->('a -> 'a)->'a->'a"
- "while == (LAM b g. fix$(LAM f x.
- If b$x then f$(g$x) else x fi))"
+ "while = (LAM b g. fix$(LAM f x. If b$x then f$(g$x) else x fi))"
(* ------------------------------------------------------------------------- *)
(* access to definitions *)