Searched defs:beq (Results 1 - 5 of 5) sorted by relevance

/seL4-l4v-master/HOL4/src/HolSat/vector_def_CNF/
H A DdefCNF.sml32 val beq = mk_thy_const{Name = "=", Ty = bool --> bool --> bool, Thy = "min"} value
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaMath.sml665 val beq = prove( value
/seL4-l4v-master/HOL4/src/metis/
H A DnormalForms.sml39 val beq = ``$= : bool->bool->bool``; value
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DlzConv.sml1748 then let val beq = bubble l' rhs value
/seL4-l4v-master/HOL4/src/1/
H A DConv.sml2394 val beq = bubble l' rhs value

Completed in 70 milliseconds