src/HOLCF/ex/loop.thy

ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
they can be proved trivially using eq_cs
ZF/domrange/XXX_empty: renamed XXX_0

(*  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