1877 section {* Conclusion *}

  1877 section {* Conclusion *}

  1878 

  1878 

  1879 text {*

  1879 text {*

  1880   We have presented an extension for Nominal Isabelle in order to derive a

  1880   We have presented an extension for Nominal Isabelle in order to derive a

  1881   convenient reasoning infrastructure for term-constructors binding multiple

  1881   convenient reasoning infrastructure for term-constructors binding multiple

  1883   Core-Haskell. For such calculi, we can also derive strong induction

  1883   Core-Haskell. For such calculi, we can also derive strong induction

  1884   principles that have the usual variable already built in. At the moment we

  1884   principles that have the usual variable already built in. At the moment we

  1885   can do so only with some manual help, but future work will automate them

  1885   can do so only with some manual help, but future work will automate them

  1886   completely.  The code underlying this extension will become part of the

  1886   completely.  The code underlying this extension will become part of the

  1887   Isabelle distribution, but for the moment it can be downloaded from the

  1887   Isabelle distribution, but for the moment it can be downloaded from the