*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Abbreviation makes Isabelle/HOL very slow*From*: Giuliano Losa <giuliano at losa.fr>*Date*: Tue, 23 Aug 2016 10:00:40 -0400*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Icedove/45.2.0

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**

**Follow-Ups**:**Re: [isabelle] Abbreviation makes Isabelle/HOL very slow***From:*Thomas Sewell

- Previous by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Date: [isabelle] WG:AW: Abbreviation makes Isabelle/HOL very slow
- Previous by Thread: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Thread: Re: [isabelle] Abbreviation makes Isabelle/HOL very slow
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list