[isabelle-dev] datatype takes minutes, but timing panel shows 10s

[Andreas Lochbihler]

Hi Dmitriy,

> the code plugin defines a new constant (copy of op =) that is used as equality.
>
> datatype x = A | B
> export_code equal_x_inst.equal_x in SML
This is precisely the instantiation of the equals type class.

> To get it executable (#constructors)^2 equations are proved in a backward fashion (I'm
> sure it could be easilly done in a forward fashion as well). However, this code goes back
> to Stefan and Florian, and we didn't attempt to optimize it when integrating it with the
> new package.
I see.

> But isn't the performance now (894d6d863823 ) already acceptable?
I have not tried it yet, because I am busy testing Isabelle2015-RC0.

Cheers,
Andreas