equal
deleted
inserted
replaced
112 "0 * x = 0" |
112 "0 * x = 0" |
113 "1 * x = x" |
113 "1 * x = x" |
114 "x + y = y + x" |
114 "x + y = y + x" |
115 by auto} |
115 by auto} |
116 |
116 |
117 val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ |
117 val real_linarith_proc = |
118 "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc |
118 Simplifier.make_simproc @{context} "fast_real_arith" |
|
119 {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}], |
|
120 proc = K Lin_Arith.simproc, identifier = []} |
119 |
121 |
120 |
122 |
121 (* setup *) |
123 (* setup *) |
122 |
124 |
123 val _ = |
125 val _ = |