[isabelle] programming internal proofs



The Isabelle reference manual says that Tactic.prove should be used to
perform programmed proofs.  

(If I use functions such as prove_goal, I get nasty messages about
using obsolete goal commands.)

Unfortunately, the latest CVS version of Isabelle no longer has such a
function in the Tactic structure. 

So what should I be using instead?

Michael.






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