> On 15 May 2018, at 14:51, Makarius wrote:
>
> Maybe also a campaign to get rid of unnecessary syntax ambiguity.
Totally. Most of the time it is completely unnecessary
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On 12/05/18 11:40, Lawrence Paulson wrote:
> I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are
> ancient. They desperately need updating and streamlining.
>
> We’ve decided that Group-Ring-Module is irremediable, and are using it
> only as a list of useful results that need
On 15/05/18 14:31, Fabian Immler wrote:
>
> I did move FuncSet back to HOL-Library in isabelle/2af1f142f855 and
> afp/5d961e9f8536.
> It seems like this improved the performance a lot:
>
> isabelle/2af1f142f855
> afp/5d961e9f8536
Great, I have seen already 2af1f142f855 "move FuncSet back to
> Am 14.05.2018 um 13:24 schrieb Fabian Immler :
>
> I did notice that those changes caused issues with timeouts in some AFP
> sessions, and simply "fixed" those on the spot (e.g., the ones in afp/85324e3
> and afp/2ff575e hinted at problems caused by incorporating syntax for