1signature BoolExtractShared = 2sig 3 4include Abbrev 5 6val dest_neg_eq : term -> term * term 7val is_neg_eq : term -> bool 8val mk_neg___idempot : term -> term 9val eq_sym_aconv : term -> term -> bool 10 11 12val BOOL_EQ_IMP_CONV : conv; 13val BOOL_NEG_PAIR_CONV : conv; 14val BOOL_EXTRACT_SHARED_CONV : conv; 15 16val BOOL_EQ_IMP_convdata : simpfrag.convdata 17val BOOL_EXTRACT_SHARED_convdata : simpfrag.convdata; 18val BOOL_NEG_PAIR_convdata : simpfrag.convdata; 19 20 21end 22