Lines Matching defs:opr
189 fun mk_binop opr (l,r) =
190 Term.list_mk_comb(opr,[l,r]) handle HOL_ERR _ => failwith "mk_binop"
192 fun list_mk_binop opr = Lib.end_itlist (Lib.curry (mk_binop opr));
194 fun dest_binop opr tm =
196 val (opr',lhs) = Term.dest_comb Rator
198 if opr=opr' then (lhs,rhs) else fail()
202 fun strip_binop opr =
203 let val dest = dest_binop opr
213 fun binops opr =
214 let val dest = dest_binop opr
223 fun is_binop opr = Lib.can (dest_binop opr)