[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
makarius at sketis.net
Sun Nov 8 18:59:21 CET 2015
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
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
More information about the isabelle-dev