[isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword
- To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword
- From: Christoph LANGE <math.semantic.web at gmail.com>
- Date: Thu, 03 Oct 2013 20:04:09 +0100
- Organization: University of Birmingham
- Sender: Christoph Lange <allegristas at gmail.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130919 Thunderbird/17.0.9
in Isabelle 2013 when I wrote "statement try", or try0, and try found a
proof, clicking on this proof in the output panel replaced the "try"
keyword in the edited source by the proof. This is no longer the case
in 2013-1-RC1. Instead the proof (e.g. "by blast") is placed after the
"try", which remains.
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
This archive was generated by a fusion of
Pipermail (Mailman edition) and