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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
