diff options
author | Josh Chen | 2020-05-26 16:50:13 +0200 |
---|---|---|
committer | Josh Chen | 2020-05-26 16:50:13 +0200 |
commit | 028f43a0737128024742234f3ee95b24986d6403 (patch) | |
tree | 566ea92495d93db334fda605af1e8e598cf4bc41 /spartan/core/Spartan.thy | |
parent | 8ba8357a0b4640a3be817fd0645d026b568bc552 (diff) |
1. New congruence declarations for calculational reasoning. 2. Remove old elimination tactic.
Diffstat (limited to '')
-rw-r--r-- | spartan/core/Spartan.thy | 12 |
1 files changed, 5 insertions, 7 deletions
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> |