Re: [isabelle] On Recursion Induction
On 05/08/2012 01:03 PM, Alfio Martini wrote:
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
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.
when in theory mode (i.e., not inside a proof), or like
when in proof mode. (I don't know if it is possible to set it in "prove"
mode however ;)).
hope this helps
This archive was generated by a fusion of
Pipermail (Mailman edition) and