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.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
