match scratch_window#sequent_viewer#get_selected_terms with
[] ->
C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
+ ("<h1 color=\"red\">No terms selected</h1>")
| terms ->
try
let expr = tactic terms scratch_window#term in
let left = call_tactic ProofEngine.left
let right = call_tactic ProofEngine.right
let assumption = call_tactic ProofEngine.assumption
+ let injection = call_tactic_with_input ProofEngine.injection
+ let discriminate = call_tactic_with_input ProofEngine.discriminate
let generalize =
call_tactic_with_goal_inputs
(ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)