Re: [isabelle] Announcing Isabelle2013-2

Le Fri, 06 Dec 2013 12:00:51 +0100, Makarius <makarius at> a écrit:

Isabelle2013-2 is now available.

I found what is I believe an issue with Sledgehammer and its “Isar proofs” option.

In the test theory below (also as attached file), if I move the caret next to “using r1 r2” then in the Sledgehammer pan, check “Isar proofs”, then click “Apply”, something strange happens: if first run up to displaying a proof, then something appears in the output pan saying “ENTER MATCH”, then the 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.


    theory Test
    imports BNF

      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


“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.thy
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.