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



2013-10-03 20:04 Christoph LANGE:
> 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.

After some more playing I'm starting to realise that this might be a
_feature_.  Suppose you try to prove something with Sledgehammer, and it
suggests several possibilities, which you would then minimise, all
possibilities are retained in the document until you finally decide for
one proof.  However you would have to clean up yourself all those
alternatives you don't like.

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.