Wolfgang Jeltsch (Nov 08 2021 at 12:57): Wolfgang Jeltsch (Nov 08 2021 at 12:57):When executing a proof method expression m, n, failure of n triggers backtracking, possibly resulting in m picking a different proof. How can I achieve that failure of n results in only n and the proof methods before msearching for alternative proofs, so that m is not reconsidering it’s choice of proof?
Last updated: Dec 28 2025 at 02:03 UTC