[isabelle] Large datatype definition: measuring elapsed time


I'm formalizing the syntax of IPv6 Addresses.

I made a quite large datatype.


The datatype definition is loading on my laptop within some minutes.

However, when I ctrl+hover the datatype command, it tells me:
  command "datatype"
  32.453s elapsed time, 42.494s cpu time, 11.460s GC time

Sitting there with a stop watch, it took more than 3 minutes. Is this
a bug in the time measurement of datatype?

In general, is there a way to speed up the datatype definition?


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