Re: [isabelle-dev] HOL-Algebra
Hi all, just a few comments on my behalf. >> We’ve decided that Group-Ring-Module is irremediable, and are using it >> only as a list of useful results that need to be done again. Seems to make sense. > Just one oddity in HOL-Algebra: It claims canonical theory names like> > "Group", "Ring", "Module". Thus the main HOL session needs to evade via> non-standard names "Groups", "Rings", "Modules" (the latter is new in> 2af1f142f855). This pragmatic tradition had been started by »Orderings.thy«; I'm uncertain whether it is worth the effort to change it. Note that the theories »More_*.thy« contain material contributed by Jeremy Avigad but not situated in HOL-Algebra in the first place; when collecting this I did not want to touch the original theories, but as part of a rework those theories could be integrated. 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
Re: [isabelle-dev] Slowdown of ConcurrentGC
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
