Re: [isabelle] datatype definition performance



Tobias and Stefan write:
>...Quick and Dirty mode...

ah, that's much better, many thanks.  It seems our Isabelle2005 has that
unset by default, whereas the Isabelle2004 has it set.

(still, 9 minutes to really prove those theorems seems quite a while -
for curiosity, is it known how this should scale with the numbers of
mutually-recursive types and of constructors?)

Peter









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.