src/Provers/classical.ML
changeset 46459 73823dbbecc4
parent 45375 7fe19930dfc9
child 46874 993c413746f4
equal deleted inserted replaced
46458:19ef91d7fbd4 46459:73823dbbecc4
   668 
   668 
   669 (*compose a tactic alternatively before/after the step tactic *)
   669 (*compose a tactic alternatively before/after the step tactic *)
   670 fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
   670 fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
   671 fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
   671 fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
   672 
   672 
   673 fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
   673 fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
   674 fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
   674 fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
   675 fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   675 fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   676 fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   676 fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   677 
   677 
   678 
   678 
   679 
   679