author | clasohm |
Tue, 06 Feb 1996 12:42:31 +0100 | |
changeset 1479 | 21eb5e156d91 |
parent 1274 | ea0668a1c0ba |
child 2642 | 3c3a84cc85a9 |
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" defs 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