author | huffman |
Sat, 04 Jun 2005 02:24:47 +0200 | |
changeset 16232 | 8a12e11d222b |
parent 14981 | e73f8140af78 |
child 17291 | 94f6113fe9ed |
permissions | -rw-r--r-- |
(* Title: HOLCF/ex/Loop.thy ID: $Id$ Author: Franz Regensburger Theory for a loop primitive like while *) Loop = Tr + Fix + 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