author | wenzelm |
Sun, 30 Jul 2000 13:02:14 +0200 | |
changeset 9473 | 7d13a5ace928 |
parent 244 | 929fc2c63bd0 |
permissions | -rw-r--r-- |
(* 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