[isabelle-dev] datatype_new problem

[Christian Sternagel]

Sorry, I forgot. This refers to Isabelle c07bac41c7ab

cheers

chris

On 07/14/2014 12:56 PM, Christian Sternagel wrote:
> Dear Jasmin,
>
> consider the following datatype specification
>
>    datatype_new 'f f =
>      F1 'f 'f 'f 'f |
>      F2 'f 'f 'f 'f
>
> (which takes about 1 second with Isabelle2014-RC0) does not terminate
> within a few minutes anymore.
>
> Note that this is a minimal example that originates from IsaFoR
>
> http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/2a9fc552f074/IsaFoR/Nonloop_SRS_Impl.thy#l214
>
>
> and does not terminate within 10 hours on Cezary's machine.
>
> I did not have time to do a proper bisect until now. Maybe you could
> have a look ;)
>
> cheers
>
> chris