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

[Clemens Ballarin]

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.

Clemens


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