not_leE -> not_le_imp_less and other tidying
authorpaulson <lp15@cam.ac.uk>
Thu Dec 10 13:38:40 2015 +0000 (2015-12-10)
changeset 61824dcbe9f756ae0
parent 61823 5daa82ba4078
child 61825 69b035408b18
not_leE -> not_le_imp_less and other tidying
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Disjoint_Sets.thy
src/HOL/List.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Orderings.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/WFair.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Dec 07 10:49:08 2015 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Thu Dec 10 13:38:40 2015 +0000
     1.3 @@ -413,11 +413,11 @@
     1.4  
     1.5  lemma less_cSupD:
     1.6    "X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
     1.7 -  by (metis less_cSup_iff not_leE bdd_above_def)
     1.8 +  by (metis less_cSup_iff not_le_imp_less bdd_above_def)
     1.9  
    1.10  lemma cInf_lessD:
    1.11    "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
    1.12 -  by (metis cInf_less_iff not_leE bdd_below_def)
    1.13 +  by (metis cInf_less_iff not_le_imp_less bdd_below_def)
    1.14  
    1.15  lemma complete_interval:
    1.16    assumes "a < b" and "P a" and "\<not> P b"
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Dec 07 10:49:08 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Dec 10 13:38:40 2015 +0000
     2.3 @@ -2335,7 +2335,7 @@
     2.4    thus ?th1 ?th2
     2.5      using Float_representation_aux[of m e]
     2.6      unfolding x_def[symmetric]
     2.7 -    by (auto dest: not_leE)
     2.8 +    by (auto dest: not_le_imp_less)
     2.9  qed
    2.10  
    2.11  lemma ln_shifted_float:
     3.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Mon Dec 07 10:49:08 2015 +0100
     3.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Thu Dec 10 13:38:40 2015 +0000
     3.3 @@ -79,7 +79,7 @@
     3.4    "(\<And>n. A n \<subseteq> A (Suc n)) \<Longrightarrow> disjoint_family (\<lambda>i. A (Suc i) - A i)"
     3.5    using lift_Suc_mono_le[of A]
     3.6    by (auto simp add: disjoint_family_on_def)
     3.7 -     (metis insert_absorb insert_subset le_SucE le_antisym not_leE less_imp_le)
     3.8 +     (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less less_imp_le)
     3.9  
    3.10  lemma disjoint_family_on_disjoint_image:
    3.11    "disjoint_family_on A I \<Longrightarrow> disjoint (A ` I)"
     4.1 --- a/src/HOL/List.thy	Mon Dec 07 10:49:08 2015 +0100
     4.2 +++ b/src/HOL/List.thy	Thu Dec 10 13:38:40 2015 +0000
     4.3 @@ -3958,7 +3958,7 @@
     4.4  lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
     4.5  apply (case_tac "k \<le> i")
     4.6   apply  (simp add: min_def)
     4.7 -apply (drule not_leE)
     4.8 +apply (drule not_le_imp_less)
     4.9  apply (simp add: min_def)
    4.10  apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
    4.11   apply  simp
     5.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Mon Dec 07 10:49:08 2015 +0100
     5.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Thu Dec 10 13:38:40 2015 +0000
     5.3 @@ -875,7 +875,7 @@
     5.4  apply (subst RepAbs_matrix)
     5.5  apply auto
     5.6  apply (simp add: Suc_le_eq)
     5.7 -apply (rule not_leE)
     5.8 +apply (rule not_le_imp_less)
     5.9  apply (subst nrows_le)
    5.10  by simp
    5.11  qed
    5.12 @@ -891,7 +891,7 @@
    5.13  apply (subst RepAbs_matrix)
    5.14  apply auto
    5.15  apply (simp add: Suc_le_eq)
    5.16 -apply (rule not_leE)
    5.17 +apply (rule not_le_imp_less)
    5.18  apply (subst ncols_le)
    5.19  by simp
    5.20  qed
     6.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Mon Dec 07 10:49:08 2015 +0100
     6.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Dec 10 13:38:40 2015 +0000
     6.3 @@ -25,7 +25,7 @@
     6.4      \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
     6.5    by (metis (no_types) abs_ge_zero
     6.6        algebra_simps mult.comm_neutral
     6.7 -      mult_nonpos_nonneg not_leE order_trans zero_less_one)
     6.8 +      mult_nonpos_nonneg not_le_imp_less order_trans zero_less_one)
     6.9  
    6.10  (*** Now various verions with an increasing shrink factor ***)
    6.11  
    6.12 @@ -686,7 +686,7 @@
    6.13   apply simp
    6.14   apply (subst abs_of_nonneg)
    6.15    apply (drule_tac x = x in spec) back
    6.16 -  apply (metis diff_less_0_iff_less linorder_not_le not_leE xt1(12) xt1(6))
    6.17 +  apply (metis diff_less_0_iff_less linorder_not_le not_le_imp_less xt1(12) xt1(6))
    6.18   apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
    6.19  by (metis abs_ge_zero linorder_linear max.absorb1 max.commute)
    6.20  
     7.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 07 10:49:08 2015 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Dec 10 13:38:40 2015 +0000
     7.3 @@ -9,21 +9,6 @@
     7.4  imports Brouwer_Fixpoint Operator_Norm Uniform_Limit
     7.5  begin
     7.6  
     7.7 -lemma netlimit_at_vector: (* TODO: move *)
     7.8 -  fixes a :: "'a::real_normed_vector"
     7.9 -  shows "netlimit (at a) = a"
    7.10 -proof (cases "\<exists>x. x \<noteq> a")
    7.11 -  case True then obtain x where x: "x \<noteq> a" ..
    7.12 -  have "\<not> trivial_limit (at a)"
    7.13 -    unfolding trivial_limit_def eventually_at dist_norm
    7.14 -    apply clarsimp
    7.15 -    apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
    7.16 -    apply (simp add: norm_sgn sgn_zero_iff x)
    7.17 -    done
    7.18 -  then show ?thesis
    7.19 -    by (rule netlimit_within [of a UNIV])
    7.20 -qed simp
    7.21 -
    7.22  declare has_derivative_bounded_linear[dest]
    7.23  
    7.24  subsection \<open>Derivatives\<close>
     8.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 07 10:49:08 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Dec 10 13:38:40 2015 +0000
     8.3 @@ -12,24 +12,47 @@
     8.4  begin
     8.5  
     8.6  lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
     8.7 -  fixes S :: "real set"
     8.8 +  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
     8.9    shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
    8.10    apply (auto simp add: abs_le_iff intro: cSup_least)
    8.11    by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
    8.12  
    8.13  lemma cInf_abs_ge:
    8.14 -  fixes S :: "real set"
    8.15 -  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
    8.16 -  using cSup_abs_le [of "uminus ` S"]
    8.17 -  by (fastforce simp add: Inf_real_def)
    8.18 +  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
    8.19 +  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
    8.20 +  shows "\<bar>Inf S\<bar> \<le> a"
    8.21 +proof -
    8.22 +  have "Sup (uminus ` S) = - (Inf S)"
    8.23 +  proof (rule antisym)
    8.24 +    show "- (Inf S) \<le> Sup(uminus ` S)"
    8.25 +      apply (subst minus_le_iff)
    8.26 +      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
    8.27 +      apply (subst minus_le_iff)
    8.28 +      apply (rule cSup_upper, force)
    8.29 +      using bdd apply (force simp add: abs_le_iff bdd_above_def)
    8.30 +      done
    8.31 +  next
    8.32 +    show "Sup (uminus ` S) \<le> - Inf S"
    8.33 +      apply (rule cSup_least)
    8.34 +       using \<open>S \<noteq> {}\<close> apply (force simp add: )
    8.35 +      apply clarsimp  
    8.36 +      apply (rule cInf_lower)
    8.37 +      apply assumption
    8.38 +      using bdd apply (simp add: bdd_below_def)
    8.39 +      apply (rule_tac x="-a" in exI)
    8.40 +      apply force
    8.41 +      done
    8.42 +  qed
    8.43 +  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
    8.44 +qed
    8.45  
    8.46  lemma cSup_asclose:
    8.47 -  fixes S :: "real set"
    8.48 +  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
    8.49    assumes S: "S \<noteq> {}"
    8.50      and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
    8.51    shows "\<bar>Sup S - l\<bar> \<le> e"
    8.52  proof -
    8.53 -  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
    8.54 +  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
    8.55      by arith
    8.56    have "bdd_above S"
    8.57      using b by (auto intro!: bdd_aboveI[of _ "l + e"])
    8.58 @@ -53,26 +76,6 @@
    8.59      by (simp add: Inf_real_def)
    8.60  qed
    8.61  
    8.62 -lemma cSup_finite_ge_iff:
    8.63 -  fixes S :: "real set"
    8.64 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Sup S \<longleftrightarrow> (\<exists>x\<in>S. a \<le> x)"
    8.65 -  by (metis cSup_eq_Max Max_ge_iff)
    8.66 -
    8.67 -lemma cSup_finite_le_iff:
    8.68 -  fixes S :: "real set"
    8.69 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Sup S \<longleftrightarrow> (\<forall>x\<in>S. a \<ge> x)"
    8.70 -  by (metis cSup_eq_Max Max_le_iff)
    8.71 -
    8.72 -lemma cInf_finite_ge_iff:
    8.73 -  fixes S :: "real set"
    8.74 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
    8.75 -  by (metis cInf_eq_Min Min_ge_iff)
    8.76 -
    8.77 -lemma cInf_finite_le_iff:
    8.78 -  fixes S :: "real set"
    8.79 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
    8.80 -  by (metis cInf_eq_Min Min_le_iff)
    8.81 -
    8.82  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    8.83    scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
    8.84    scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
    8.85 @@ -87,7 +90,6 @@
    8.86  lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
    8.87  lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
    8.88  lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
    8.89 -lemma conjunctD5: assumes "a \<and> b \<and> c \<and> d \<and> e" shows a b c d e using assms by auto
    8.90  
    8.91  declare norm_triangle_ineq4[intro]
    8.92  
    8.93 @@ -5145,17 +5147,11 @@
    8.94            done
    8.95        }
    8.96        assume as': "p \<noteq> {}"
    8.97 -      from real_arch_simple[of "Sup((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
    8.98 +      from real_arch_simple[of "Max((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
    8.99        then have N: "\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N"
   8.100 -        apply (subst(asm) cSup_finite_le_iff)
   8.101 -        using as as'
   8.102 -        apply auto
   8.103 -        done
   8.104 +        by (meson Max_ge as(1) dual_order.trans finite_imageI tagged_division_of_finite)
   8.105        have "\<forall>i. \<exists>q. q tagged_division_of (cbox a b) \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
   8.106 -        apply rule
   8.107 -        apply (rule tagged_division_finer[OF as(1) d(1)])
   8.108 -        apply auto
   8.109 -        done
   8.110 +        by (auto intro: tagged_division_finer[OF as(1) d(1)])
   8.111        from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
   8.112        have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)"
   8.113          apply (rule setsum_nonneg)
     9.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 07 10:49:08 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Dec 10 13:38:40 2015 +0000
     9.3 @@ -2560,6 +2560,21 @@
     9.4    shows "netlimit (at x within S) = x"
     9.5    using assms by (metis at_within_interior netlimit_at)
     9.6  
     9.7 +lemma netlimit_at_vector:
     9.8 +  fixes a :: "'a::real_normed_vector"
     9.9 +  shows "netlimit (at a) = a"
    9.10 +proof (cases "\<exists>x. x \<noteq> a")
    9.11 +  case True then obtain x where x: "x \<noteq> a" ..
    9.12 +  have "\<not> trivial_limit (at a)"
    9.13 +    unfolding trivial_limit_def eventually_at dist_norm
    9.14 +    apply clarsimp
    9.15 +    apply (rule_tac x="a + scaleR (d / 2) (sgn (x - a))" in exI)
    9.16 +    apply (simp add: norm_sgn sgn_zero_iff x)
    9.17 +    done
    9.18 +  then show ?thesis
    9.19 +    by (rule netlimit_within [of a UNIV])
    9.20 +qed simp
    9.21 +
    9.22  
    9.23  text\<open>Useful lemmas on closure and set of possible sequential limits.\<close>
    9.24  
    10.1 --- a/src/HOL/Orderings.thy	Mon Dec 07 10:49:08 2015 +0100
    10.2 +++ b/src/HOL/Orderings.thy	Thu Dec 10 13:38:40 2015 +0000
    10.3 @@ -82,7 +82,7 @@
    10.4    "a \<noteq> top \<longleftrightarrow> a \<prec> top"
    10.5    by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
    10.6  
    10.7 -end  
    10.8 +end
    10.9  
   10.10  
   10.11  subsection \<open>Syntactic orders\<close>
   10.12 @@ -97,7 +97,7 @@
   10.13    less_eq  ("(_/ <= _)" [51, 51] 50) and
   10.14    less  ("op <") and
   10.15    less  ("(_/ < _)"  [51, 51] 50)
   10.16 -  
   10.17 +
   10.18  notation (xsymbols)
   10.19    less_eq  ("op \<le>") and
   10.20    less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   10.21 @@ -149,13 +149,13 @@
   10.22  text \<open>Transitivity.\<close>
   10.23  
   10.24  lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
   10.25 -by (auto simp add: less_le_not_le intro: order_trans) 
   10.26 +by (auto simp add: less_le_not_le intro: order_trans)
   10.27  
   10.28  lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
   10.29 -by (auto simp add: less_le_not_le intro: order_trans) 
   10.30 +by (auto simp add: less_le_not_le intro: order_trans)
   10.31  
   10.32  lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
   10.33 -by (auto simp add: less_le_not_le intro: order_trans) 
   10.34 +by (auto simp add: less_le_not_le intro: order_trans)
   10.35  
   10.36  
   10.37  text \<open>Useful for simplification, but too risky to include by default.\<close>
   10.38 @@ -360,8 +360,7 @@
   10.39  lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
   10.40  unfolding not_less .
   10.41  
   10.42 -(*FIXME inappropriate name (or delete altogether)*)
   10.43 -lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
   10.44 +lemma not_le_imp_less: "\<not> y \<le> x \<Longrightarrow> x < y"
   10.45  unfolding not_le .
   10.46  
   10.47  text \<open>Dual order\<close>
   10.48 @@ -516,11 +515,11 @@
   10.49     is not a parameter of the locale. *)
   10.50  
   10.51  declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
   10.52 -  
   10.53 +
   10.54  declare order_refl  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.55 -  
   10.56 +
   10.57  declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.58 -  
   10.59 +
   10.60  declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.61  
   10.62  declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.63 @@ -528,9 +527,9 @@
   10.64  declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.65  
   10.66  declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.67 -  
   10.68 +
   10.69  declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.70 -  
   10.71 +
   10.72  declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.73  
   10.74  declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
   10.75 @@ -950,7 +949,7 @@
   10.76    "(x::'a::order) > y ==> y > z ==> x > z"
   10.77    "(a::'a::order) >= b ==> a ~= b ==> a > b"
   10.78    "(a::'a::order) ~= b ==> a >= b ==> a > b"
   10.79 -  "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c" 
   10.80 +  "a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c"
   10.81    "a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c"
   10.82    "a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
   10.83    "a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
   10.84 @@ -990,11 +989,11 @@
   10.85  
   10.86  lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
   10.87  
   10.88 -(* 
   10.89 +(*
   10.90    Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
   10.91    for the wrong thing in an Isar proof.
   10.92  
   10.93 -  The extra transitivity rules can be used as follows: 
   10.94 +  The extra transitivity rules can be used as follows:
   10.95  
   10.96  lemma "(a::'a::order) > z"
   10.97  proof -
   10.98 @@ -1145,7 +1144,7 @@
   10.99      with \<open>f x \<le> f y\<close> show False by simp
  10.100    qed
  10.101  qed
  10.102 -  
  10.103 +
  10.104  lemma strict_mono_less:
  10.105    assumes "strict_mono f"
  10.106    shows "f x < f y \<longleftrightarrow> x < y"
  10.107 @@ -1317,10 +1316,10 @@
  10.108  
  10.109  end
  10.110  
  10.111 -class no_top = order + 
  10.112 +class no_top = order +
  10.113    assumes gt_ex: "\<exists>y. x < y"
  10.114  
  10.115 -class no_bot = order + 
  10.116 +class no_bot = order +
  10.117    assumes lt_ex: "\<exists>y. y < x"
  10.118  
  10.119  class unbounded_dense_linorder = dense_linorder + no_top + no_bot
    11.1 --- a/src/HOL/UNITY/SubstAx.thy	Mon Dec 07 10:49:08 2015 +0100
    11.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Dec 10 13:38:40 2015 +0000
    11.3 @@ -361,7 +361,7 @@
    11.4  apply (simp add: Image_singleton, clarify)
    11.5  apply (case_tac "m<l")
    11.6   apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
    11.7 -apply (blast intro: not_leE subset_imp_LeadsTo)
    11.8 +apply (blast intro: not_le_imp_less subset_imp_LeadsTo)
    11.9  done
   11.10  
   11.11  
    12.1 --- a/src/HOL/UNITY/WFair.thy	Mon Dec 07 10:49:08 2015 +0100
    12.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Dec 10 13:38:40 2015 +0000
    12.3 @@ -488,7 +488,7 @@
    12.4  apply clarify
    12.5  apply (case_tac "m<l")
    12.6   apply (blast intro: leadsTo_weaken_R diff_less_mono2)
    12.7 -apply (blast intro: not_leE subset_imp_leadsTo)
    12.8 +apply (blast intro: not_le_imp_less subset_imp_leadsTo)
    12.9  done
   12.10  
   12.11  
    13.1 --- a/src/HOL/Word/Word.thy	Mon Dec 07 10:49:08 2015 +0100
    13.2 +++ b/src/HOL/Word/Word.thy	Thu Dec 10 13:38:40 2015 +0000
    13.3 @@ -3599,7 +3599,7 @@
    13.4        apply (simp (no_asm), arith)
    13.5       apply (simp (no_asm), arith)
    13.6      apply (rule notI [THEN notnotD],
    13.7 -           drule leI not_leE,
    13.8 +           drule leI not_le_imp_less,
    13.9             drule sbintrunc_inc sbintrunc_dec,      
   13.10             simp)+
   13.11    done