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

2013-11-13 13:14 bnord:
> 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?

There was an earlier conversation about this, in which I first
complained but then found out that it's actually sometimes useful (at
least with sledgehammer), and Makarius also commented on it.  The thread
starts here:
(2013-1-RC1: proof method suggested try or try0 no longer overwrites
'try' keyword)



Christoph Lange, Enterprise Information Systems Department
Applied Computer Science @ University of Bonn; Fraunhofer IAIS, Skype duke4701

→ Web Intelligence, Mining and Semantics (WIMS), Thessaloniki, Greece,
  2–4 June 2014.  Submission until 9 Dec.

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