[isabelle] Isabelle 2013 / Print goals on failed proof method


I am posting this as a reminder for me and other people who get bitten
by some annoying behaviour of Isabelle 2013 which I describe below (and
cannot switch to a more current version of Isabelle).

Due to some external libraries I use, I am currently stuck on Isabelle
2013. As Peter already mentioned a few months ago (here or on
isabelle-dev), when a tactic fails, it prints all subgoals, independent
of the goals_limit option (I tried setting it with "declare" before the
proof and with "using" in the proof).

When the goal is large (in my current example: 41 subgoals, with up to
60-70 lines each), these take very long to print (around 6 minutes on my
8-core i7 machine).

As a work-around, I modified src/Pure/Isar/proof_display.ML, setting
"limit = true" in the function "string_of_goal", thus making it honour
the goal_limit option.

  -- Lars

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.