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
> 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
(2013-1-RC1: proof method suggested try or try0 no longer overwrites
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