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:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-October/thread.html#00013
(2013-1-RC1: proof method suggested try or try0 no longer overwrites
'try' keyword)

Cheers,

Christoph

-- 
Christoph Lange, Enterprise Information Systems Department
Applied Computer Science @ University of Bonn; Fraunhofer IAIS
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Web Intelligence, Mining and Semantics (WIMS), Thessaloniki, Greece,
  2–4 June 2014.  Submission until 9 Dec.  http://wims14.csd.auth.gr




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