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

[Makarius]

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