*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Announcing Isabelle2013-2*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Sat, 21 Dec 2013 13:55:34 +0100*Organization*: Ada @ Home*References*: <alpine.LNX.2.00.1312061159540.43347@lxbroy10.informatik.tu-muenchen.de> <op.w8flicsjule2fv@cardamome>*User-agent*: Opera Mail/12.16 (Linux)

Test_2.thy (also as attached file): theory Test_2 imports BNF begin declare [[rule_trace]] type_synonym 'a pp = "['a, 'a] ⇒ bool" inductive ppinduct :: "'a pp ⇒ 'a list pp" for f where r1: "ppinduct f [] []" | r2: "⟦f h1 h2; ppinduct f t1 t2⟧ ⟹ ppinduct f (h1 # t1) (h2 # t2)" lemma "ppinduct f (h # t) [] ⟹ False" using r1 r2 end

Le Fri, 06 Dec 2013 12:00:51 +0100, Makarius <makarius at sketis.net> a écrit:Isabelle2013-2 is now available.I found what is I believe an issue with Sledgehammer and its “Isarproofs”option.In the test theory below (also as attached file), if I move the caretnextto “using r1 r2” then in the Sledgehammer pan, check “Isar proofs”, then click “Apply”, something strange happens: if first run up to displaying aproof, then something appears in the output pan saying “ENTER MATCH”,thenthe content in the Sledgehammer pan disappears then the content of the output pan is back to what is was just before it displayed “ENTER MATCH” and Sledgehammer continue running and cannot be stopped with “Cancel”. The issue does not occur if “Isar proofs” is not checked. Test.thy: theory Test imports BNF begin declare [[rule_trace]] type_synonym 'a pp = "['a, 'a] ⇒ bool" inductive ppinduct :: "'a pp ⇒ 'a list pp" where r1: "ppinduct _ [] []"| r2: "⟦f h1 h2; ppinduct f t1 t2⟧ ⟹ ppinduct f (h1 # t1) (h2 #t2)"lemma "ppinduct f (h # t) [] ⟹ False" using r1 r2 end

-- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**Attachment:
Test_2.thy**

**References**:**[isabelle] Announcing Isabelle2013-2***From:*Makarius

**Re: [isabelle] Announcing Isabelle2013-2***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Announcing Isabelle2013-2
- Next by Date: [isabelle] My unforgivable soundness issue with a locale
- Previous by Thread: Re: [isabelle] Announcing Isabelle2013-2
- Next by Thread: [isabelle] Proof method to split disjunctions and conjunctions ?
- Cl-isabelle-users December 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