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