diff options
| author | Josh Chen | 2020-05-25 15:21:02 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-25 15:21:02 +0200 |
| commit | 3de65af4b59e6d3cc8e74acecf704beccd54b774 (patch) | |
| tree | e5b7a89c5b22d49915d9266c7aaf27d825ce4271 /spartan/theories | |
| parent | 3ad2f03f7dbc922e2c711241146db091d193003d (diff) | |
new elimination tactic
Diffstat (limited to 'spartan/theories')
| -rw-r--r-- | spartan/theories/Spartan.thy | 20 |
1 files changed, 3 insertions, 17 deletions
diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy index ab2606e..744e219 100644 --- a/spartan/theories/Spartan.thy +++ b/spartan/theories/Spartan.thy @@ -165,20 +165,6 @@ lemmas [comps] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong -ML \<open> -val ctxt = @{context}; -val typing = @{term "t: \<Sum>x: A. B x"}; -val insts = []; -let - val (eterm, typing) = Lib.dest_typing typing - val (rl, tms) = the (Elim.lookup_rule ctxt (Term.head_of typing)) -in - Drule.infer_instantiate @{context} - (tms ~~ map (Thm.cterm_of ctxt) (eterm::insts)) - rl -end -\<close> - ML_file \<open>../lib/tactics.ML\<close> method_setup assumptions = @@ -195,13 +181,13 @@ method_setup intro = method_setup intros = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close> -method_setup elim' = +method_setup old_elim = \<open>Scan.option Args.term >> (fn tm => fn ctxt => - SIMPLE_METHOD' (SIDE_CONDS (elims_tac tm ctxt) ctxt))\<close> + SIMPLE_METHOD' (SIDE_CONDS (old_elims_tac tm ctxt) ctxt))\<close> method_setup elim = \<open>Scan.repeat Args.term >> (fn tms => fn ctxt => - SIMPLE_METHOD' (SIDE_CONDS (elim_tac' tms ctxt) ctxt))\<close> + CONTEXT_METHOD (K (elim_context_tac tms ctxt 1)))\<close> method elims = elim+ |