Lines Matching defs:MAX
131 val MAX =
133 ("MAX",
134 ���$MAX x y = (if x < y then y else x)���,
140 ���(!x y. x <= x MAX y) /\ (!x y. y <= x MAX y)���,
141 RW_TAC arith_ss [MAX]
146 ���!x y. (SUC x MAX SUC y) = SUC(x MAX y)���,
147 RW_TAC arith_ss [MAX]
152 ���!x y z. ((x MAX y) <= z) = ((x <= z) /\ (y <= z))���,
153 RW_TAC arith_ss [MAX]
162 (HEIGHT_obj1 (UPDATE1 a l m) = SUC (HEIGHT_obj1 a MAX HEIGHT_method1 m))
164 (HEIGHT_dict1 (CONS e d) = SUC (HEIGHT_entry1 e MAX HEIGHT_dict1 d)) /\