From 3922e24270518be67192ad6928bb839132c74c07 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 23 Sep 2020 17:03:42 +0200 Subject: Basic experiments adding reduction to the type checker --- spartan/core/eqsubst.ML | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'spartan/core/eqsubst.ML') diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML index 31d5126..5ae8c73 100644 --- a/spartan/core/eqsubst.ML +++ b/spartan/core/eqsubst.ML @@ -430,12 +430,12 @@ val _ = Method.setup \<^binding>\sub\ (parser >> (fn ((asm, occs), inthms) => fn ctxt => SIMPLE_METHOD' ( (if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms))) - "single-step substitution" #> + "single-step substitution" (* #> Method.setup \<^binding>\subst\ (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS 0 ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms))))) - "single-step substitution with automatic discharge of side conditions" + "single-step substitution with automatic discharge of side conditions" *) ) end -- cgit v1.2.3