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. 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.”  “Structured Programming supports the law of the excluded muddle.”  : Epigrams on Programming — Alan J. — P. Yale University
Description: Binary data