test/Tools/isac/MathEngBasic/tactic.sml
Sat, 30 Nov 2019 15:43:14 +0100 lucin: prep. next_tactic_result, Accept_Tac2 takes ctxt in addition