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