[isabelle] Recommended use of try and try0



Dear all,

I learned about the "try" and "try0" tools to search for proof methods.
 Now I wonder what's the right way of using them.

When "try0" says that, e.g. "by fastforce" is the fastest way to prove
something, does this automatically mean that I should _use_ "by
fastforce"?  Or are there hidden traps?

More generally, is it a recommended practice to occasionally revisit my
proofs, replace "by <some automated method>" by "try" everywhere, and
then generally use the proof methods that "try" recommends?

Thanks in advance for your help,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 7–12 Jul, Bath, UK; Deadline 12 Mar
  http://cicm-conference.org/2013/
→ SePublica Workshop @ ESWC 2013.  Montpellier, France, 26-30 May.
  Deadline 14 Mar; http://sepublica.mywikipaper.org
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  3–5 April 2013, Exeter, UK.  3 Hands-on Tutorials on Economics
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/





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