simple composition : ";", sequential application of tactic
general composition: tac;[tac1 ...tacn] : apply tac1 ... tacn to subgoal 1 to n generated from tac
orelse composition: "tac1tac2" , apply tac1 first, only if it fail can we apply tac2
idtac tactic : dont change
fail tactic: tac;fail can only fail if tac generate a new sub goal
try tactic: "try tac " equal to "tac;idtac" which means that if fail,nothing change
没有评论:
发表评论