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
>> 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
>
>
>


-- 
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 MHonArc.