A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.

Christian Urban, Stefan Berghofer

Browse the full CADE paper archive.