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