Hi Makarius,

> I have studied this a bit further. The interval
> 75130777ece4:d45b78cb86cf contains more than just the string type
> change, but it is still the main thing. Here are also other sessions in
> similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498:
>   * faster: HOL-IMP, HOL-Quickcheck_Examples,
>     Network_Security_Policy_Verification, Pre_Perron_Frobenius,
>     JiveDataStoreModel, Partial_Function_MR
>   * slower: Tarskis_Geometry, XML, Cauchy

distangling the ancient misunderstaning of char in Isabelle vs. various
character-related types in several target languages may indeed come at a
certain price in exotic situations; anyway I will have a look at those
sessions whether something meaningful can be derived from them.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to