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

(limited to 'hott/Identity.thy')

diff --git a/hott/Identity.thy b/hott/Identity.thy
index b9ebafb..b06604f 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -54,7 +54,7 @@ section \<open>Path induction\<close>
 
 method_setup eq =
   \<open>Args.term >> (fn tm => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (
+    CHEADGOAL o SIDE_CONDS 0 (
       CONTEXT_SUBGOAL (fn (goal, i) => fn cst as (ctxt, st) =>
         let
           val facts = Proof_Context.facts_of ctxt
-- 
cgit v1.2.3