[isabelle] Recommended use of try and try0
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 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
→ 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and