--- a/src/HOL/Int.thy Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Int.thy Fri Aug 19 05:49:09 2022 +0000
@@ -652,7 +652,7 @@
"nat (of_bool P) = of_bool P"
by auto
-lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
+lemma split_nat [linarith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
(is "?P = (?L \<and> ?R)")
for i :: int
proof (cases "i < 0")
@@ -739,11 +739,11 @@
text \<open>
This version is proved for all ordered rings, not just integers!
- It is proved here because attribute \<open>arith_split\<close> is not available
+ It is proved here because attribute \<open>linarith_split\<close> is not available
in theory \<open>Rings\<close>.
But is it really better than just rewriting with \<open>abs_if\<close>?
\<close>
-lemma abs_split [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))"
+lemma abs_split [linarith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))"
for a :: "'a::linordered_idom"
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)