Theory Ex4

Up to index of Isabelle/LCF/ex

theory Ex4
imports LCF
uses [Ex4.ML]
begin

header {* Prefixpoints *}

theory Ex4
imports LCF
begin

end

theorem example:

  [| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f) = p