replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
(*** 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