From 710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 3 Aug 2020 13:34:53 +0200
Subject: (FEAT) SIDE_CONDS tactical has additional argument specifying how
 many initial subgoals to skip applying the side condition solver to.

(FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type.

(FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method.
---
 spartan/core/eqsubst.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'spartan/core/eqsubst.ML')

diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML
index e7ecf63..31d5126 100644
--- a/spartan/core/eqsubst.ML
+++ b/spartan/core/eqsubst.ML
@@ -433,7 +433,7 @@ val _ =
         "single-step substitution" #>
       Method.setup \<^binding>\<open>subst\<close>
         (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD (
-          CHEADGOAL o SIDE_CONDS
+          CHEADGOAL o SIDE_CONDS 0
             ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms)))))
         "single-step substitution with automatic discharge of side conditions"
     )
-- 
cgit v1.2.3