1signature schneiderUtils =
2  sig
3    type term = Term.term
4    type thm = Thm.thm
5    type goal = Abbrev.goal
6    type conv = Abbrev.conv
7    type tactic = Abbrev.tactic
8
9    val APPLY_ASM_TAC : int -> tactic -> tactic
10    val ASM_LIST_TAC : int list
11                       -> (thm list -> term list * 'a -> 'b)
12                          -> term list * 'a -> 'b
13    val ASM_TAC : int -> (thm -> term list * 'a -> 'b) -> term list * 'a -> 'b
14    val BOOL_VAR_ELIM_CONV : term -> term -> thm
15    val BOOL_VAR_ELIM_TAC : term -> tactic
16    val COND_FUN_EXT_CONV : term -> thm
17    val COND_FUN_EXT_TAC : tactic
18    val COPY_ASM_NO : int -> tactic
19    val FORALL_IN_CONV : conv
20    val FORALL_UNFREE_CONV : term -> thm
21    val LEFT_CONJ_TAC : tactic
22    val LEFT_DISJ_TAC : tactic
23    val LEFT_EXISTS_TAC : tactic
24    val LEFT_FORALL_TAC : term -> tactic
25    val LEFT_LEMMA_DISJ_CASES_TAC : thm -> tactic
26    val LEFT_NO_EXISTS_TAC : int -> tactic
27    val LEFT_NO_FORALL_TAC : int -> term -> tactic
28    val MP2_TAC : thm -> goal -> (term list * term) list * (thm list -> thm)
29    val MY_MP_TAC : term -> goal -> (term list * term) list * (thm list -> thm)
30    val POP_NO_ASSUM : int -> (thm -> term list * 'a -> 'b) -> term list * 'a -> 'b
31    val POP_NO_TAC : int -> tactic
32    val PROP_TAC : tactic
33    val REW_PROP_TAC : tactic
34    val RIGHT_CONJ_TAC : tactic
35    val RIGHT_DISJ_TAC : tactic
36    val RIGHT_LEMMA_DISJ_CASES_TAC : thm -> tactic
37    val REWRITE1_TAC : thm -> tactic
38    val SELECT_EXISTS_TAC : term -> tactic
39    val SELECT_UNIQUE_RULE : term -> thm -> thm -> thm
40    val SELECT_UNIQUE_TAC : tactic
41    val SELECT_UNIQUE_THM : thm
42    val TAC_CONV : tactic -> term -> thm
43    val UNDISCH_ALL_TAC : tactic
44    val UNDISCH_HD_TAC : tactic
45    val UNDISCH_NO_TAC : int -> tactic
46    val delete : int -> 'a list -> 'a list
47    val elem : int -> 'a list -> 'a
48    val prove_thm : string * term * tactic -> thm
49  end
50