1signature probLib =
2sig
3  type term = Term.term
4  type thm = Thm.thm
5
6  val SEQUENCE_CASES_TAC : term -> Abbrev.tactic
7  val SEQ_CASES_TAC      : term frag list -> Abbrev.tactic
8
9  val prob_canon_ss : simpLib.simpset
10
11  val PROB_PSEUDO_SHD_CONV : term -> thm;
12  val PROB_PSEUDO_STL_CONV : term -> thm;
13
14  val PROB_UNIF_CONV        : term -> thm;
15  val PROB_UNIFORM_CUT_CONV : term -> thm;
16
17end
18