--- a/src/HOLCF/ex/loop.thy Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title: HOLCF/ex/loop.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Theory for a loop primitive like while
-*)
-
-Loop = Tr2 +
-
-consts
-
- step :: "('a -> tr)->('a -> 'a)->'a->'a"
- while :: "('a -> tr)->('a -> 'a)->'a->'a"
-
-rules
-
- step_def "step == (LAM b g x. If b[x] then g[x] else x fi)"
- while_def "while == (LAM b g. fix[LAM f x.\
-\ If b[x] then f[g[x]] else x fi])"
-
-
-end
-