1signature bagSimpleLib =
2sig
3  include Abbrev
4
5  val BAG_RESORT_CONV : int list -> conv
6  val BAG_IMAGE_CONV  : conv
7  val GET_BAG_IN_THMS : term -> thm list
8
9  val get_resort_position___pred       : (term -> bool) -> term -> int option
10  val get_resort_list___pred           : (term -> bool) -> term -> int list
11  val get_resort_positions___pred_pair : (term -> term -> bool) -> term -> term -> (int * int) option
12  val get_resort_lists___pred_pair     : (term -> term -> bool) -> term -> term -> (int list * int list)
13
14  val SIMPLE_BAG_NORMALISE_CONV  : conv
15  val BAG_EQ_INSERT_CANCEL_CONV  : conv
16  val BAG_DIFF_INSERT_CANCEL_CONV: conv
17  val SUB_BAG_INSERT_CANCEL_CONV : conv
18  val SUB_BAG_INSERT_SOLVE       : term -> thm
19
20end
21