Lines Matching defs:threshold
209 threshold (:'t # 'w) =
231 let t = threshold (:'t # 'w) in
264 let t = threshold (:'t # 'w) in
1399 `ulp (:'t # 'w) < threshold (:'t # 'w)`,
2706 ulp (:'t # 'w) < 2 * abs x /\ abs x < threshold (:'t # 'w) ==>
2844 ulp (:'t # 'w) < 2 * abs x /\ abs x < threshold (:'t # 'w) ==>
2969 ulp (:'t # 'w) < abs x /\ abs x < threshold (:'t # 'w) ==>
3197 0 < threshold (:'t # 'w)
3216 threshold (:'t # 'w) <= x ==>
3224 x <= -threshold (:'t # 'w) ==>
3405 val threshold = Q.store_thm("threshold",
3406 `threshold (:'t # 'w) =
3458 largest (:'t # 'w) < threshold (:'t # 'w)
3460 rw [largest, threshold, realTheory.REAL_LT_RDIV, realTheory.REAL_LT_LMUL,