From 12eed8685674b7d5ff7bc45a44a061e01f99ce5f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 21 Jul 2020 02:09:44 +0200
Subject: 1. Type-checking/inference now more principled, and the
 implementation is better. 2. Changed most tactics to context tactics.

---
 spartan/core/elimination.ML | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/spartan/core/elimination.ML b/spartan/core/elimination.ML
index 11b3af9..cd4e414 100644
--- a/spartan/core/elimination.ML
+++ b/spartan/core/elimination.ML
@@ -34,13 +34,13 @@ fun register_rule tms rl =
   in Rules.map (Termtab.update (hd, (rl, map (#1 o dest_Var) tms))) end
 
 
-(* [elims] attribute *)
+(* [elim] attribute *)
 val _ = Theory.setup (
-  Attrib.setup \<^binding>\<open>elims\<close>
+  Attrib.setup \<^binding>\<open>elim\<close>
     (Scan.repeat Args.term_pattern >>
       (Thm.declaration_attribute o register_rule))
     ""
-  #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elims\<close>,
+  #> Global_Theory.add_thms_dynamic (\<^binding>\<open>elim\<close>,
       fn context => (map #1 (rules (Context.proof_of context))))
 )
 
-- 
cgit v1.2.3