# Theory Ex3

Up to index of Isabelle/LCF/ex

theory Ex3
imports LCF
uses [Ex3.ML]
begin

    (* $Id: Ex3.thy,v 1.2 2005/09/03 15:54:11 wenzelm Exp $ *)

    header {* Addition with fixpoint of successor *}

    theory Ex3
    imports LCF
    begin

    consts
      s     :: "'a => 'a"
      p     :: "'a => 'a => 'a"

    axioms
      p_strict:     "p(UU) = UU"
      p_s:          "p(s(x),y) = s(p(x,y))"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem example:

      p(FIX(s), y) = FIX(s)