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

Clemens Ballarin ballarin at in.tum.de
Wed Nov 18 21:20:34 CET 2015

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.

I did check that this change does not accidentally change any of the Isabelle documentation.  I also ran Makarius' termination stress test on Isabelle and the AFP.  The latter needed timeout_scale=8.


On 08 November, 2015 18:59 CET, Makarius <makarius at sketis.net> wrote: 
> 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:
>    [RIPEMD-160-SPARK] is still on FAIL.
>    [ShortestPath] is still on FAIL.
>    [Graph_Theory] is still on FAIL.
>    Full entry status at http://afp.sourceforge.net/status.shtml
>    AFP version: development -- hg id f433a3e7bbf1
>    Isabelle version: devel -- hg id 15952a05133c
>  	Makarius

More information about the isabelle-dev mailing list