*To*: æåå <lyj238 at ios.ac.cn>*Subject*: Re: [isabelle] A proof on moreover and ultimately*From*: Wenda Li <wl302 at cam.ac.uk>*Date*: Tue, 29 Dec 2015 13:00:32 +0000*Cc*: isabelle-users at cl.cam.ac.uk, æåå <duankq at ios.ac.cn>*In-reply-to*: <6524ebdc76fa4e23a8cb4fabdd95b600@EX01.ios.ac.cn>*References*: <6524ebdc76fa4e23a8cb4fabdd95b600@EX01.ios.ac.cn>*User-agent*: Roundcube Webmail/1.0.2

Hi Yongjian,

Cheers, Wenda On 2015-12-29 06:00, æåå wrote:

Dear experts: I meet a problem on a proof of a typical case analysis, whose structure is as follows: have "case1 \or case2 \or ....\or casen" by auto ---------------------------------- moreover {assume "case1" proof_1 have "?P" } ...... moreover {assume "case162" proof_n have "?P" } ultimately show âïP" all 162 moreovers are finished, but the last ultimately command cann't be finished? why? is there is a limit on the number of subcases (moreovers)? The proof is in the on_inis.thy, which is attached regards! yongjian Li

-- Wenda Li PhD Candidate Computer Laboratory University of Cambridge

**Follow-Ups**:**Re: [isabelle] A proof on moreover and ultimately***From:*Manuel Eberl

**References**:

- Previous by Date: Re: [isabelle] Starting soonâ Verified Firewall Ruleset Verification
- Next by Date: Re: [isabelle] A proof on moreover and ultimately
- Previous by Thread: [isabelle] A proof on moreover and ultimately
- Next by Thread: Re: [isabelle] A proof on moreover and ultimately
- Cl-isabelle-users December 2015 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