--- a/src/HOL/Deriv.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Deriv.thy Tue Feb 23 16:25:08 2016 +0100
@@ -962,7 +962,7 @@
fix h::real
assume "0 < h" "h < s"
with all [of h] show "f x < f (x+h)"
- proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+ proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
with l
have "0 < (f (x+h) - f x) / h" by arith
@@ -991,7 +991,7 @@
fix h::real
assume "0 < h" "h < s"
with all [of "-h"] show "f x < f (x-h)"
- proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+ proof (simp add: abs_if pos_less_divide_eq split add: if_split_asm)
assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
with l
have "0 < (f (x-h) - f x) / h" by arith