From 720da0f918118388d114e09664b129d2b29be2b1 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 22 May 2020 15:43:14 +0200
Subject: some tweaks and comments, in preparation for general inductive type
 elimination

---
 spartan/lib/tactics.ML | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'spartan/lib/tactics.ML')

diff --git a/spartan/lib/tactics.ML b/spartan/lib/tactics.ML
index 0e09533..c72947a 100644
--- a/spartan/lib/tactics.ML
+++ b/spartan/lib/tactics.ML
@@ -104,8 +104,7 @@ fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS
 fun intros_tac ctxt = SUBGOAL (fn (_, i) =>
   (CHANGED o REPEAT o CHANGED o intro_tac ctxt) i)
 
-(* Basic elimination tactic *)
-(*Only uses existing type judgments from the context
+(*Basic elimination tactic, only uses existing type judgments from the context
   (performs no type synthesis)*)
 fun elims_tac opt_tm ctxt = case opt_tm of
     NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (Elim.rules ctxt) i)
-- 
cgit v1.2.3