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