[isabelle-dev] datatype_new problem

[Jasmin Christian Blanchette]

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