From 028f43a0737128024742234f3ee95b24986d6403 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 26 May 2020 16:50:13 +0200
Subject: 1. New congruence declarations for calculational reasoning. 2. Remove
 old elimination tactic.

---
 spartan/core/Spartan.thy | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'spartan/core/Spartan.thy')

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 50002a6..1d93885 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -8,8 +8,9 @@ imports
 keywords
   "Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and
   "focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
-  "derive" "prems" "vars":: quasi_command and
-  "print_coercions" :: thy_decl
+  "congruence" "print_coercions" :: thy_decl and
+  "rhs" "derive" "prems" "vars" :: quasi_command
+  
 
 begin
 
@@ -154,7 +155,8 @@ ML_file \<open>focus.ML\<close>
 
 section \<open>Congruence automation\<close>
 
-(*Potential to be retired*)
+consts "rhs" :: \<open>'a\<close> ("..")
+
 ML_file \<open>congruence.ML\<close>
 
 
@@ -186,10 +188,6 @@ method_setup intro =
 method_setup intros =
   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close>
 
-method_setup old_elim =
-  \<open>Scan.option Args.term >> (fn tm => fn ctxt =>
-    SIMPLE_METHOD' (SIDE_CONDS (old_elims_tac tm ctxt) ctxt))\<close>
-
 method_setup elim =
   \<open>Scan.repeat Args.term >> (fn tms => fn ctxt =>
     CONTEXT_METHOD (K (elim_context_tac tms ctxt 1)))\<close>
-- 
cgit v1.2.3