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
     1 (*  Title:      HOLCF/ex/Loop.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Theory for a loop primitive like while
     6 *)
     7 
     8 Loop = Tr +
     9 
    10 consts
    11         step  :: "('a -> tr)->('a -> 'a)->'a->'a"
    12         while :: "('a -> tr)->('a -> 'a)->'a->'a"
    13 
    14 defs
    15 
    16   step_def      "step == (LAM b g x. If b$x then g$x else x fi)"
    17   while_def     "while == (LAM b g. fix$(LAM f x.
    18                    If b$x then f$(g$x) else x fi))"
    19 
    20 end
    21