Re: [isabelle] 2014-RC1 issues

-----Original Message-----
From: Lars Noschinski <noschinl at>
Sender: cl-isabelle-users-bounces at
Date: Wed, 30 Jul 2014 13:42:01 
To: cl-isabelle-users at<cl-isabelle-users at>
Subject: 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 "" *})


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