(*<*)

theory Paper

imports "../Nominal/Test"

begin

(*>*)

section {* Introduction *}

text {*

  It has not yet fared so well in the POPLmark challenge

  as the second part contain a formalisation of records 

  where ...

  The difficulty can be appreciated by considering that the

  definition given by Leroy in [] is incorrect (it omits a

  side-condition).

  Contributions:  We provide definitions for when terms

  involving general bindings are alpha-equivelent.

*}

text {*

  Acknowledgements: We thank Andrew Pitts for the many discussions

  about the topic. We thank Peter Sewell for making [] available 

  to us and explaining some of the finer points of the OTT tool.

*}

(*<*)

end

(*>*)