--- a/src/HOL/ex/FinFunPred.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/ex/FinFunPred.thy Tue Feb 23 16:25:08 2016 +0100
@@ -142,7 +142,7 @@
lemma finfun_Ball_except_update:
"finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)"
-by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: split_if_asm)
+by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: if_split_asm)
lemma finfun_Ball_except_update_code [code]:
fixes a :: "'a :: card_UNIV"
@@ -169,7 +169,7 @@
lemma finfun_Bex_except_update:
"finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P"
-by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: split_if_asm)
+by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: if_split_asm)
lemma finfun_Bex_except_update_code [code]:
fixes a :: "'a :: card_UNIV"
@@ -265,4 +265,4 @@
end
declare iso_finfun_Ball_Ball[code_unfold del]
-end
\ No newline at end of file
+end