[isabelle-dev] datatype_new problem

Christian Sternagel c.sternagel at gmail.com
Mon Jul 14 12:56:11 CEST 2014

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


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 ;)



More information about the isabelle-dev mailing list