author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 14981 | e73f8140af78 |
child 16232 | 8a12e11d222b |
permissions | -rw-r--r-- |
(* Title: HOLCF/ex/Loop.thy ID: $Id$ Author: Franz Regensburger Theory for a loop primitive like while *) Loop = Tr + 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