equal
deleted
inserted
replaced
212 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
212 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
213 |
213 |
214 val hypreal_mult_mono_thms = |
214 val hypreal_mult_mono_thms = |
215 [(rotate_prems 1 hypreal_mult_less_mono2, |
215 [(rotate_prems 1 hypreal_mult_less_mono2, |
216 cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), |
216 cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), |
217 (hypreal_mult_le_mono2, |
217 (mult_left_mono, |
218 cvar(hypreal_mult_le_mono2, hd(tl(prems_of hypreal_mult_le_mono2))))] |
218 cvar(mult_left_mono, hd(tl(prems_of mult_left_mono))))] |
219 |
219 |
220 in |
220 in |
221 |
221 |
222 val hypreal_arith_setup = |
222 val hypreal_arith_setup = |
223 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
223 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |