src/LCF/ex/Ex2.thy

converted UNITY/Comp/{AllocImpl,Client} to Isar scripts

(***  Example 3.8  ***)

Ex2 = LCF +

consts
  P	:: "'a => tr"
  F	:: "'a => 'a"
  G	:: "'a => 'a"
  H	:: "'a => 'b => 'b"
  K	:: "('a => 'b => 'b) => ('a => 'b => 'b)"

rules
  F_strict	"F(UU) = UU"
  K		"K = (%h x y. P(x) => y | F(h(G(x),y)))"
  H		"H = FIX(K)"

end