From c530305cbcafba9f66f1a55a1b5177a62f52535c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 5 Aug 2020 15:21:43 +0200
Subject: 1. fix intros method. 2. Couple extra lemmas; good small test cases
 for normalization in typechecking/elaboration.

---
 spartan/core/Spartan.thy         | 3 ++-
 spartan/core/context_tactical.ML | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'spartan')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index ea72208..7f13036 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -248,7 +248,8 @@ method_setup intros =
     K (CONTEXT_METHOD (fn facts =>
       case n_opt of
         SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))
-      | NONE => CREPEAT (CCHANGED (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))))))\<close>
+      | NONE => CCHANGED (CREPEAT (CCHANGED (
+          CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)))))))\<close>
 
 method_setup elim =
   \<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD (
diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML
index 0aa6f20..d0fed61 100644
--- a/spartan/core/context_tactical.ML
+++ b/spartan/core/context_tactical.ML
@@ -92,7 +92,7 @@ fun CREPEAT ctac =
 
 fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
 
-fun CREPEAT_N 0 _ = all_ctac
+fun CREPEAT_N 0 _ = no_ctac
   | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac
 
 fun CFILTER pred ctac cst =
-- 
cgit v1.2.3