--- a/src/HOL/Transcendental.thy Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Transcendental.thy Tue Feb 23 18:04:31 2016 +0100
@@ -4265,11 +4265,11 @@
lemma cos_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
using cos_gt_zero_pi [of x]
- by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+ by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
- by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
+ by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: if_split_asm)
lemma tan_mono_le: "-(pi/2) < x ==> x \<le> y ==> y < pi/2 \<Longrightarrow> tan(x) \<le> tan(y)"
using less_eq_real_def tan_monotone by auto
@@ -4284,7 +4284,7 @@
lemma tan_bound_pi2: "\<bar>x\<bar> < pi/4 \<Longrightarrow> \<bar>tan x\<bar> < 1"
using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
- by (auto simp: abs_if split: split_if_asm)
+ by (auto simp: abs_if split: if_split_asm)
lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
by (simp add: tan_def sin_diff cos_diff)