[isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword



Hi Makarius,

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.

Cheers,

Christoph

-- 
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.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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