Lines Matching defs:mode
36 val mode = Term.mk_var ("mode", rounding_ty)
106 real_to_fp_var & mode == float_to_fp o' real_to_float & mode)
118 real_to_fp_var & mode ==
119 mk_I_hashhash float_to_fp o' real_to_float_with_flags & mode)
131 v & mode & a ==
132 real_to_fp & mode & (intrealSyntax.real_of_int_tm & a))
144 v & mode == (float_to_int & mode) o' fp_to_float)
160 (Term.mk_var (s, rounding_ty --> ty1) & mode,
161 Term.mk_const (f, rounding_ty --> ty2) & mode)
221 val x = tm & mode & (fp_to_float & a) & (fp_to_float & b)
224 v & mode & a & b ==
269 val x = tm & mode & (fp_to_float & a) & (fp_to_float & b) &
273 v & mode & a & b & c ==
358 |> try_f (Thm.SPEC ``mode:rounding``)