1signature Rules =
2sig
3 type ('a,'b) subst = ('a,'b)Lib.subst
4 type term = Term.term
5 type thm = Thm.thm
6
7
8  val RIGHT_ASSOC      : thm -> thm
9  val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
10
11  val CHOOSE           : term * thm -> thm -> thm
12  val EXISTS           : term * term -> thm -> thm
13  val EXISTL           : term list -> thm -> thm
14  val IT_EXISTS        : (term,term) subst -> thm -> thm
15
16  val EVEN_ORS         : thm list -> thm list
17  val DISJ_CASESL      : thm -> thm list -> thm
18
19  val LEFT_ABS_VSTRUCT : thm -> thm
20  val LEFT_EXISTS      : thm -> thm
21
22  val SUBS             : thm list -> thm -> thm
23  val simpl_conv       : thm list -> term -> thm
24  val simplify         : thm list -> thm -> thm
25
26end
27