[isabelle] Abbreviation makes Isabelle/HOL very slow



Hello,
in the following theory, the processing of the definition of x2 takes
minutes on my machine.

theory Test
imports Main
begin

abbreviation x1 where "x1 f â f"

definition x2 where "x2 â x"

end

If I remove the abbreviation, it becomes instantaneous.

I came across this problem because I made the following abbreviation:

abbreviation flip where "flip f â Î x y . f y x"

It rendered Isabelle unusable, as the processing of some commands (not
only definition, but also other commands) started to take minutes.

I fixed the problem by using a definition instead of an abbreviation,
but there might be something worth investigating going on here.

I observed this behavior using Isabelle-2016 and Isabelle_15-Aug-2016.

Giuliano

Attachment: signature.asc
Description: OpenPGP digital signature



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