src/Tools/isac/Interpret/tactic.sml
changeset 59512 e504168e7b01
parent 59499 19add1fb3225
child 59533 aa8b25bb8ebb
     1.1 --- a/src/Tools/isac/Interpret/tactic.sml	Thu Mar 07 16:50:20 2019 +0100
     1.2 +++ b/src/Tools/isac/Interpret/tactic.sml	Thu Mar 07 17:22:20 2019 +0100
     1.3 @@ -318,7 +318,6 @@
     1.4    This is useful for costly results, e.g. from rewriting;
     1.5    however, these results might be changed by Scripts like
     1.6        "      eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
     1.7 -      "      eq = drop_questionmarks eq;" ^
     1.8        "      eq = (Rewrite_Set equival_trans False) eq;" ^
     1.9    TODO.WN120106 ANALOGOUSLY TO Substitute':
    1.10    So tac_ contains the term t the result was calculated from