Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

I have now committed this. See isabelle/e89cfc004f18; the AFP didn't require changes. The final version does not activate abbreviations as aggressively as my first proposal. This was necessary so abbreviations are not propagated over rewrite morphisms, which would have been very confusing.

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

Hi Clemens, > I'm not familiar with the termination argument for abbreviations, but certainly we can say that abbreviations define a reduction system (in fact a rewrite system), and I would assume that there are no cycles and infinite paths. Now my patch will clone part of this system,

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

On Sat, 7 Nov 2015, Makarius wrote: Since the actual change to src/Pure/Isar/generic_target.ML is so small, we should just go ahead with it -- after a full test with AFP. The option "timeout_scale" from Isabelle/a2f0f659a3c2 should help to do this. Note that AFP is presently a bit broken:

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

On Fri, 6 Nov 2015, Makarius wrote: On Wed, 4 Nov 2015, Clemens Ballarin wrote: On 30 October, 2015 20:02 CET, Makarius wrote: > Standard batch build prints relatively few terms, so this is not yet > significant as a test. > > The following change prints every

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

On Wed, 4 Nov 2015, Clemens Ballarin wrote: On 30 October, 2015 20:02 CET, Makarius wrote: Standard batch build prints relatively few terms, so this is not yet significant as a test. The following change prints every intermediate Isar toplevel state. With that I get

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

On Thu, 29 Oct 2015, Florian Haftmann wrote: I have not spend any thoughts whether there could be terminaton issues. Is there any argument beyond the absence of counterexamples that that can never happen? Standard batch build prints relatively few terms, so this is not yet significant as a

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

»const_decl« is shared by different primitives and operations on various targets. Hence the patch looks fine. The »revert_abbrev« goes back to changeset 2b86fac03ec5 in named_target.ML, although the guarding criterion has changed over time. 2b86fac03ec5 is already in the highly experimental

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

Hi Clemens, thanks for undertaking this. I will have a look at this and give feedback. Cheers, Florian Am 27.10.2015 um 18:59 schrieb Clemens Ballarin: > Related to the below discussion on isabelle-users, I have now refined the > patch I had circulated then. Here is the NEWS entry: >

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

Related to the below discussion on isabelle-users, I have now refined the patch I had circulated then. Here is the NEWS entry: * More gentle suppression of syntax along locale morphisms while printing terms. Previously 'abbreviation' and 'notation' declarations would be suppressed for