Re: [isabelle] 2014-RC1 issues



On 30.07.2014 10:26, Peter Lammich wrote:
> Here is a list of issues that I encountered with RC1:
>
And yet another issue: A method executing

   error ""

produces an error marker in the right sidebar. However, the associated
apply command does not get underlined in red and the error marker in the
left sidebar is missing.

Reproduce with:

theory Scratch imports Pure begin

lemma "PROP P"
  apply (tactic {* error "" *})
  oops

end




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