[isabelle-dev] datatype_new problem
c.sternagel at gmail.com
Mon Jul 14 12:56:11 CEST 2014
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