1signature bagSyntax = 2sig 3 include Abbrev 4 5 val EMPTY_BAG_tm : term 6 val BAG_DIFF_tm : term 7 val SUB_BAG_tm : term 8 val BAG_INSERT_tm : term 9 val BAG_UNION_tm : term 10 val BAG_IMAGE_tm : term 11 val BAG_CARD_tm : term 12 val BAG_ALL_DISTINCT_tm : term 13 val BAG_EVERY_tm : term 14 15 val is_bag_ty : hol_type -> bool 16 val bag_ty : hol_type 17 18 val base_type : term -> hol_type 19 val list_mk_union : term list -> term 20 val mk_diff : term * term -> term 21 val mk_sub_bag : term * term -> term 22 val dest_sub_bag : term -> term * term 23 val is_sub_bag : term -> bool 24 val is_diff : term -> bool 25 val dest_diff : term -> term * term 26 val mk_union : term * term -> term 27 val list_mk_insert : term list * term -> term 28 val mk_insert : term * term -> term 29 val dest_union : term -> term * term 30 val strip_union : term -> term list 31 val is_insert : term -> bool 32 val dest_insert : term -> term * term 33 val is_union : term -> bool 34 val mk_image : term * term -> term 35 val dest_image : term -> term * term 36 val is_image : term -> bool 37 val is_empty : term -> bool 38 val mk_all_distinct : term -> term 39 val dest_all_distinct : term -> term 40 val is_all_distinct : term -> bool 41 val mk_card : term -> term 42 val dest_card : term -> term 43 val is_card : term -> bool 44 val mk_every : term * term -> term 45 val dest_every : term -> term * term 46 val is_every : term -> bool 47 48 val mk_bag : term list * hol_type -> term 49 val strip_insert : term -> term list * term 50 val dest_bag : term -> term list * hol_type 51 52end 53