1(* ===================================================================== *) 2(* FILE : barendregt.sig *) 3(* VERSION : 1.0 *) 4(* DESCRIPTION : Tactic to reduce proper substitution to the much *) 5(* simpler operation of naive substitution. *) 6(* *) 7(* AUTHOR : Peter Vincent Homeier *) 8(* DATE : October 24, 2000 *) 9(* COPYRIGHT : Copyright (c) 2000 by Peter Vincent Homeier *) 10(* *) 11(* ===================================================================== *) 12 13signature barendregt = 14sig 15 16type tactic = Abbrev.tactic 17 18 19(* 20val SHIFT_SIGMAS_TAC : tactic 21val MAKE_SIMPLE_SUBST_TAC : tactic 22*) 23 24val SIMPLE_SUBST_TAC : tactic 25 26end 27