equal
deleted
inserted
replaced
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 \<^emph>\<open>not\<close> themselves (in)equalities, because the latter activate |
84 \<^emph>\<open>not\<close> themselves (in)equalities, because the latter activate |
85 \<^text>\<open>fast_nat_arith_simproc\<close> 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 [linarith_split] = nat_diff_split split_min split_max |
89 |
89 |
90 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close> |
90 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close> |
91 |
91 |
92 named_theorems divide_simps "rewrite rules to eliminate divisions" |
92 named_theorems divide_simps "rewrite rules to eliminate divisions" |
93 |
93 |