src/LCF/ex/Ex1.thy

added intermediate value thms

(***  Section 10.4  ***)

Ex1 = LCF +

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

rules
  P_strict	"P(UU) = UU"
  K		"K = (%h x. P(x) => x | h(h(G(x))))"
  H		"H = FIX(K)"

end