Re: [isabelle] On Recursion Induction
Thank you Christian!
That was very helpful! Cheers
On Tue, May 8, 2012 at 2:01 AM, Christian Sternagel <c-sterna at jaist.ac.jp>wrote:
> 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
>> 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
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and