[isabelle] [Isabelle2013-1] try0/try/sledgehammer command isn't replaced when clicking on suggested method.



Hi,

in Isabelle2013-1 on OS X

typing

lemma True try0

and then clicking on the suggested "by simp" yields

lemma True try0 by simp

instead of

lemma True by simp

as in Isabelle2013. It's the same for try/sledgehammer.

Is this intended?

Best Benedikt




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