better way to define a tactic? #14
Description
Currently, I have defined a tactic as below.
Tactic Notation "my_inversion" tactic(target) :=
inversion target; subst; simpl; clear target.
However, there is a problem involving this.
I cannot use this tactic to branches if it is not defined at the beginning.
For example, I can do this where H0 is auto-generated by destructing d.
"induction d; try inversion H0."
However, I cannot do
"induction d; my_inversion H0."
This is not a severe problem because I can just replace "my_inversion" to corresponding primitive tactics.