Hi Chris, > 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.
> I did not have time to do a proper bisect until now. Maybe you could have a > look ;) Please do not waste your time bisecting things that we broke! ;) It was easy for me to track down the problem. The tactic for the new property "rel_cases" does not terminate on this example. I have disabled the generation of the property altogether (change 6bb3dd7f8097) until this is fixed. As a workaround (for this and future tactic issues), you can always try to "declare [[quick_and_dirty = true]]" right before and disable the option right afterward (and let us know of course!). Sorry for the trouble. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
