test-suite/output/Tactics.out


1
2
3
4
5
6

intro H; split; [  a H |  e H ].

intros; match goal with
        | |- context [if ?X then _ else _] => case X
        end; trivial.