Lines Matching defs:ml
2287 val ((ml,left),(mr,right)) = with_exn (dest_comb ## dest_comb) (l,r)
2293 val _ = if all (curry op= ml) [mlr,mrr,mr] then () else raise (size_err
2294 ("measures '" ^ term_to_string ml ^ "' and '" ^
2295 term_to_string (first (not o curry op= ml) [mlr,mrr,mr]) ^ "' are not equal"))
2302 (specced,ml,left,right,p_term,xvar)
2304 fun make_recursion (specced,ml,left,right,p_term,xvar) target size_thm =
2310 val measure = mk_comb(mk_const("measure",(target --> num) --> target --> target --> bool),ml)
2335 fun make_induction (specced,ml,left,right,p_term,xvar) target size_thm =
2340 val measure = mk_comb(mk_const("measure",(target --> num) --> target --> target --> bool),ml)
2344 (ISPEC ml prim_recTheory.WF_measure)))
2362 let val (specced,ml,left,right,p_term,xvar) = split_size_thm target size_thm
2370 induction = make_induction (specced,ml,left,right,p_term,xvar) target size_thm,
2371 recursion = make_recursion (specced,ml,left,right,p_term,xvar) target size_thm,