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.