*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] "show" taking very long with goals with many hypothesis, MWE*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 12 Jun 2013 09:58:22 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1371018811.4145.3.camel@kirk>*References*: <1370951829.4125.31.camel@kirk> <51B71563.7020607@inf.ethz.ch> <1370955778.4125.39.camel@kirk> <1371018811.4145.3.camel@kirk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130510 Thunderbird/17.0.6

Hi Joachim,

Andreas On 12/06/13 08:33, Joachim Breitner wrote:

Hi, Am Dienstag, den 11.06.2013, 15:02 +0200 schrieb Joachim Breitner:Sorry for not providing a minimal examplehere is one: theory Scratch imports Main begin consts foo :: "nat => bool" consts bar :: "nat => nat => nat => nat => nat => nat => nat => nat => bool" consts A :: bool consts B :: bool lemma ind_rule[case_names CaseName]: "(⋀a b c d e f g h . foo a ⟹ foo b ⟹ foo c ⟹ foo d ⟹ foo e ⟹ foo f ⟹ foo g ⟹ foo h ⟹ bar a b c d e f g h ⟹ A) ⟹ B" sorry lemma B proof (induction rule: ind_rule) case (CaseName a b c d e f g h) show A (* This takes very long *) apply (rule ccontr) sorry (* This also *) qed end Adding another parameter makes it take longer than I’d like to wait, while after removing a parameter, things are fast enough so that I woudn’t bother. Greetings, Joachim

**References**:**[isabelle] "show" taking very long with goals with many hypothesis***From:*Joachim Breitner

**Re: [isabelle] "show" taking very long with goals with many hypothesis***From:*Andreas Lochbihler

**Re: [isabelle] "show" taking very long with goals with many hypothesis***From:*Joachim Breitner

**Re: [isabelle] "show" taking very long with goals with many hypothesis, MWE***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] "show" taking very long with goals with many hypothesis, MWE
- Next by Date: [isabelle] Installation problem
- Previous by Thread: Re: [isabelle] "show" taking very long with goals with many hypothesis, MWE
- Next by Thread: [isabelle] "global" pretty printing
- Cl-isabelle-users June 2013 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