Structure bagSimpleLib

signature bagSimpleLib =
sig
  include Abbrev

  val BAG_RESORT_CONV : int list -> conv
  val BAG_IMAGE_CONV  : conv
  val GET_BAG_IN_THMS : term -> thm list

  val get_resort_position___pred       : (term -> bool) -> term -> int option
  val get_resort_list___pred           : (term -> bool) -> term -> int list
  val get_resort_positions___pred_pair : (term -> term -> bool) -> term -> term -> (int * int) option
  val get_resort_lists___pred_pair     : (term -> term -> bool) -> term -> term -> (int list * int list)

  val SIMPLE_BAG_NORMALISE_CONV  : conv
  val BAG_EQ_INSERT_CANCEL_CONV  : conv
  val BAG_DIFF_INSERT_CANCEL_CONV: conv
  val SUB_BAG_INSERT_CANCEL_CONV : conv
  val SUB_BAG_INSERT_SOLVE       : term -> thm

end

HOL 4, Kananaskis-14