1843 

  1843 

  1844 section {* Conclusion *}

  1844 section {* Conclusion *}

  1845 

  1845 

  1846 text {*

  1846 text {*

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

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

  1849   variables at once. This extension can deal with term-calculi, such as

  1849   variables at once. This extension can deal with term-calculi, such as

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

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

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

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

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

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

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

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