*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] On Recursion Induction*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Tue, 08 May 2012 14:01:01 +0900*In-reply-to*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

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.

declare [[goals_limit=20]] when in theory mode (i.e., not inside a proof), or like note [[goals_limit=20]]

hope this helps chris

**Follow-Ups**:**Re: [isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Lars Noschinski

**References**:**[isabelle] On Recursion Induction***From:*Alfio Martini

- Previous by Date: [isabelle] On Recursion Induction
- Next by Date: Re: [isabelle] On Recursion Induction
- Previous by Thread: [isabelle] On Recursion Induction
- Next by Thread: Re: [isabelle] On Recursion Induction
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list