equal
deleted
inserted
replaced
79 \<^simproc>\<open>natle_cancel_sums\<close>])\<close> |
79 \<^simproc>\<open>natle_cancel_sums\<close>])\<close> |
80 |
80 |
81 simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") = |
81 simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") = |
82 \<open>K Lin_Arith.simproc\<close> \<comment> \<open>Because of this simproc, the arithmetic solver is |
82 \<open>K Lin_Arith.simproc\<close> \<comment> \<open>Because of this simproc, the arithmetic solver is |
83 really only useful to detect inconsistencies among the premises for subgoals which are |
83 really only useful to detect inconsistencies among the premises for subgoals which are |
84 *not* themselves (in)equalities, because the latter activate |
84 \<^emph>\<open>not\<close> themselves (in)equalities, because the latter activate |
85 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the |
85 \<^text>\<open>fast_nat_arith_simproc\<close> anyway. However, it seems cheaper to activate the |
86 solver all the time rather than add the additional check.\<close> |
86 solver all the time rather than add the additional check.\<close> |
87 |
87 |
88 lemmas [arith_split] = nat_diff_split split_min split_max |
88 lemmas [arith_split] = nat_diff_split split_min split_max |
89 |
89 |
90 |
90 |