Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] programming internal proofs

view this post on Zulip Email Gateway (Aug 17 2022 at 13:28):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
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.

Last updated: May 03 2024 at 04:19 UTC