Up to index of Isabelle/LCF/ex
header {* Prefixpoints *} theory Ex4 imports LCF begin end
theorem example:
[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f) = p