Re: [isabelle] On Recursion Induction



Dear Alfio,

On 05/08/2012 01:03 PM, Alfio Martini wrote:
2) This is perhaps for Makarius: In the image  one sees that I have a total
of 11 subgoals,
but only 10 are printed. I would expect to reach the eleventh subgoal by
scrolling down in the output
window, but it does not work like that.
Actually this is independent from the interface you use. The number of subgoals that are printed is controlled by the configuration option "goals_limit" (see isar-ref p. 143). You can set it like

  declare [[goals_limit=20]]

when in theory mode (i.e., not inside a proof), or like

  note [[goals_limit=20]]

when in proof mode. (I don't know if it is possible to set it in "prove" mode however ;)).

hope this helps

chris






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