hide id, stamps;
added stamp_names_of, name_of;
replaced make_draft by prep_ext;
improved print_sg;
tuned;
(* 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"
rules
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