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/rewrite.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML
index eba0e81..99c21b5 100644
--- a/spartan/core/rewrite.ML
+++ b/spartan/core/rewrite.ML
@@ -458,7 +458,7 @@ val _ =
       "single-step rewriting, allowing subterm selection via patterns" #>
     Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >>
       (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD (
-        CHEADGOAL o SIDE_CONDS
+        CHEADGOAL o SIDE_CONDS 0
           (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms)))))
       "single-step rewriting with auto-typechecking"
   end
-- 
cgit v1.2.3