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_LAMBDAS_TAC : tactic 21 22 23val MAKE_SIMPLE_SUBST_TAC : tactic 24 25val SIMPLE_SUBST_TAC : tactic 26 27end 28