equal
deleted
inserted
replaced
25 @{thm real_of_int_inject} RS iffD2] |
25 @{thm real_of_int_inject} RS iffD2] |
26 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: |
26 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: |
27 real_of_int_less_iff RS iffD2 *) |
27 real_of_int_less_iff RS iffD2 *) |
28 |
28 |
29 in |
29 in |
30 |
|
31 val fast_real_arith_simproc = |
|
32 Simplifier.simproc (the_context ()) |
|
33 "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] |
|
34 Fast_Arith.lin_arith_prover; |
|
35 |
30 |
36 val real_arith_setup = |
31 val real_arith_setup = |
37 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
32 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
38 {add_mono_thms = add_mono_thms, |
33 {add_mono_thms = add_mono_thms, |
39 mult_mono_thms = mult_mono_thms, |
34 mult_mono_thms = mult_mono_thms, |