src/HOL/Library/Formal_Power_Series.thy

 lemma X_pow_eq_X_pow_iff [simp]:
   "(X :: ('a :: {comm_ring_1}) fps) ^ m = X ^ n \<longleftrightarrow> m = n"
 proof
   assume "(X :: 'a fps) ^ m = X ^ n"
   hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:)
-  thus "m = n" by (simp split: split_if_asm)
+  thus "m = n" by (simp split: if_split_asm)
 qed simp_all
 
 
 subsection \<open>Subdegrees\<close>
 

   assume A: "fps_cutoff n f = 0"
   thus "f = 0 \<or> n \<le> subdegree f"
   proof (cases "f = 0")
     assume "f \<noteq> 0"
     with A have "n \<le> subdegree f"
-      by (intro subdegree_geI) (auto simp: fps_eq_iff split: split_if_asm)
+      by (intro subdegree_geI) (auto simp: fps_eq_iff split: if_split_asm)
     thus ?thesis ..
   qed simp
 qed (auto simp: fps_eq_iff intro: nth_less_subdegree_zero)
 
 lemma fps_cutoff_0 [simp]: "fps_cutoff 0 f = 0"

   "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
 
 instance
 proof
   show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
-    by (simp add: dist_fps_def split: split_if_asm)
+    by (simp add: dist_fps_def split: if_split_asm)
   then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
 
   fix a b c :: "'a fps"
   consider "a = b" | "c = a \<or> c = b" | "a \<noteq> b" "a \<noteq> c" "b \<noteq> c" by blast
   then show "dist a b \<le> dist a c + dist b c"

   shows "f $ j = g $ j"
 proof (rule ccontr)
   assume "f $ j \<noteq> g $ j"
   hence "f \<noteq> g" by auto
   with assms have "i < subdegree (f - g)"
-    by (simp add: split_if_asm dist_fps_def)
+    by (simp add: if_split_asm dist_fps_def)
   also have "\<dots> \<le> j"
     using \<open>f $ j \<noteq> g $ j\<close> by (intro subdegree_leI) simp_all
   finally show False using \<open>j \<le> i\<close> by simp
 qed
 

   case True
   then show ?thesis by simp
 next
   case False
   with assms have "dist f g = inverse (2 ^ subdegree (f - g))"
-    by (simp add: split_if_asm dist_fps_def)
+    by (simp add: if_split_asm dist_fps_def)
   moreover
   from assms and False have "i < subdegree (f - g)"
     by (intro subdegree_greaterI) simp_all
   ultimately show ?thesis by simp
 qed