diff options
author | Josh Chen | 2020-09-23 17:03:42 +0200 |
---|---|---|
committer | Josh Chen | 2020-09-23 17:03:42 +0200 |
commit | 3922e24270518be67192ad6928bb839132c74c07 (patch) | |
tree | fa15b6f440a778b6804c8d3ec546188721cbd1e5 /spartan/core/eqsubst.ML | |
parent | 77df99b3ffa41395ced31785074525c85e35fee9 (diff) |
Basic experiments adding reduction to the type checker
Diffstat (limited to '')
-rw-r--r-- | spartan/core/eqsubst.ML | 4 |
1 files changed, 2 insertions, 2 deletions
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>\<open>sub\<close> (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>\<open>subst\<close> (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 |