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