src/HOLCF/ex/Loop.thy
 author kleing Mon Jun 21 10:25:57 2004 +0200 (2004-06-21) changeset 14981 e73f8140af78 parent 12036 49f6c49454c2 child 16232 8a12e11d222b permissions -rw-r--r--
Merged in license change from Isabelle2004
 clasohm@1479 ` 1` ```(* Title: HOLCF/ex/Loop.thy ``` nipkow@244 ` 2` ``` ID: \$Id\$ ``` clasohm@1479 ` 3` ``` Author: Franz Regensburger ``` nipkow@244 ` 4` nipkow@244 ` 5` ```Theory for a loop primitive like while ``` nipkow@244 ` 6` ```*) ``` nipkow@244 ` 7` slotosch@2642 ` 8` ```Loop = Tr + ``` nipkow@244 ` 9` nipkow@244 ` 10` ```consts ``` clasohm@1479 ` 11` ``` step :: "('a -> tr)->('a -> 'a)->'a->'a" ``` clasohm@1479 ` 12` ``` while :: "('a -> tr)->('a -> 'a)->'a->'a" ``` nipkow@244 ` 13` regensbu@1168 ` 14` ```defs ``` nipkow@244 ` 15` nipkow@10835 ` 16` ``` step_def "step == (LAM b g x. If b\$x then g\$x else x fi)" ``` nipkow@10835 ` 17` ``` while_def "while == (LAM b g. fix\$(LAM f x. ``` nipkow@10835 ` 18` ``` If b\$x then f\$(g\$x) else x fi))" ``` nipkow@244 ` 19` nipkow@244 ` 20` ```end ``` nipkow@244 ` 21` ``` ```