diff options
Diffstat (limited to 'spartan/core/eqsubst.ML')
| -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 |