Lines Matching refs:mr1
226 val mr1 = new_definition("mr1",
227 ���mr1 = metric(\(x,y). abs(y - x))���);
230 ���!x y. (dist mr1)(x,y) = abs(y - x)���,
231 REPEAT GEN_TAC THEN REWRITE_TAC[mr1, REWRITE_RULE[metric_tybij] ISMET_R1]
235 ���!x d. (dist mr1)(x,x + d) = abs(d)���,
239 ���!x d. (dist mr1)(x,x - d) = abs(d)���,
243 ���!x d. &0 <= d ==> ((dist mr1)(x,x + d) = d)���,
247 ���!x d. &0 <= d ==> ((dist mr1)(x,x - d) = d)���,
251 ���!x d. &0 < d ==> ((dist mr1)(x,x + d) = d)���,
256 ���!x d. &0 < d ==> ((dist mr1)(x,x - d) = d)���,
261 ���!x y z. x < z /\ (dist mr1)(x,y) < (z - x) ==> y < z���,
269 ``!x. limpt(mtop mr1) x univ(:real)``,