src/HOL/Analysis/Change_Of_Vars.thy

               by (simp add: field_simps image_comp o_def)
             ultimately show "((\<lambda>x. indicat_real S (\<chi> k. x $ k/ m k)) has_integral z *\<^sub>R \<bar>prod m UNIV\<bar>) (cbox u v)"
               by simp
             have "\<bar>z *\<^sub>R \<bar>prod m UNIV\<bar> - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar>
                  = \<bar>prod m UNIV\<bar> * \<bar>z - measure lebesgue S\<bar>"
-              by (metis (no_types, hide_lams) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib')
+              by (metis (no_types, opaque_lifting) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib')
             also have "\<dots> < e"
               using zless True by (simp add: field_simps)
             finally show "\<bar>z *\<^sub>R \<bar>prod m UNIV\<bar> - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e" .
           qed
         qed

               let ?B = "(\<lambda>(x, y). x + y) ` (f' x ` ball 0 1 \<times> ball 0 k)"
               have "bounded ?B"
                 by (simp add: bounded_plus [OF bo])
               moreover have "?rfs \<subseteq> ?B"
                 apply (auto simp: dist_norm image_iff dest!: ex_lessK)
-                by (metis (no_types, hide_lams) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball)
+                by (metis (no_types, opaque_lifting) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball)
               ultimately show "bounded (?rfs)"
                 by (rule bounded_subset)
             qed
             then have "(\<lambda>x. r *\<^sub>R x) ` ?rfs \<in> lmeasurable"
               by (simp add: measurable_linear_image)

           unfolding T_def
           proof (clarsimp simp add: Collect_conj_eq [symmetric])
             fix x
             assume "e > 0"  "m < n"  "n * e \<le> \<bar>det (matrix (f' x))\<bar>"  "\<bar>det (matrix (f' x))\<bar> < (1 + real m) * e"
             then have "n < 1 + real m"
-              by (metis (no_types, hide_lams) less_le_trans mult.commute not_le mult_le_cancel_iff2)
+              by (metis (no_types, opaque_lifting) less_le_trans mult.commute not_le mult_le_cancel_iff2)
             then show "False"
               using less.hyps by linarith
           qed
       qed auto
     qed

                       T ` {y. \<bar>y $ k - ?x' $ k\<bar> < e * min d r / (2 * real CARD('m) ^ CARD('m))}"
             proof -
               have *: "\<bar>T (b *\<^sub>R axis k 1) \<bullet> (y - x)\<bar> = b * \<bar>inv T y $ k - ?x' $ k\<bar>" for y
               proof -
                 have "\<bar>T (b *\<^sub>R axis k 1) \<bullet> (y - x)\<bar> = \<bar>(b *\<^sub>R axis k 1) \<bullet> inv T (y - x)\<bar>"
-                  by (metis (no_types, hide_lams) b_def eqb invT orthogonal_transformation_def v)
+                  by (metis (no_types, opaque_lifting) b_def eqb invT orthogonal_transformation_def v)
                 also have "\<dots> = b * \<bar>(axis k 1) \<bullet> inv T (y - x)\<bar>"
                   using \<open>b > 0\<close> by (simp add: abs_mult)
                 also have "\<dots> = b * \<bar>inv T y $ k - ?x' $ k\<bar>"
                   using orthogonal_transformation_linear [OF invT]
                   by (simp add: inner_axis' linear_diff)

         proof (rule iffI; clarsimp)
           assume b: "\<forall>e>0. \<exists>d>0. \<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and>
                                     (\<forall>y\<in>S. norm (y - x) < d \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x))"
                      (is "\<forall>e>0. \<exists>d>0. \<exists>A. ?\<Phi> e d A")
           then have "\<forall>k. \<exists>d>0. \<exists>A. ?\<Phi> (1 / Suc k) d A"
-            by (metis (no_types, hide_lams) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff)
+            by (metis (no_types, opaque_lifting) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff)
           then obtain \<delta> A where \<delta>: "\<And>k. \<delta> k > 0"
                            and Ab: "\<And>k. A k $ m $ n < b"
                            and A: "\<And>k y. \<lbrakk>y \<in> S; norm (y - x) < \<delta> k\<rbrakk> \<Longrightarrow>
                                           norm (f y - f x - A k *v (y - x)) \<le> 1/(Suc k) * norm (y - x)"
             by metis

         using orthogonal_transformation_inv [OF T] by (simp add: orthogonal_transformation_norm)
       moreover have "\<exists>t\<in>T -` P. norm (inv T x - t) \<le> e"
       proof
         have "T (inv T x - inv T t) = x - t"
           using T linear_diff orthogonal_transformation_def
-          by (metis (no_types, hide_lams) Tinv)
+          by (metis (no_types, opaque_lifting) Tinv)
         then have "norm (inv T x - inv T t) = norm (x - t)"
           by (metis T orthogonal_transformation_norm)
         then show "norm (inv T x - inv T t) \<le> e"
           using \<open>norm (x - t) \<le> e\<close> by linarith
        next

               using box_ne_empty(1) contra_subsetD [OF x(2)] mem_box(2) uv_ne by fastforce+
             moreover have "r x \<le> 1/2"
               using r12 by auto
             ultimately have "norm (v - u) \<le> 1"
               using norm_triangle_half_r [of x u 1 v]
-              by (metis (no_types, hide_lams) dist_commute dist_norm less_eq_real_def less_le_trans mem_ball)
+              by (metis (no_types, opaque_lifting) dist_commute dist_norm less_eq_real_def less_le_trans mem_ball)
             then have "norm (v - u) ^ ?n \<le> norm (v - u) ^ ?m"
               by (simp add: power_decreasing [OF mlen])
             also have "\<dots> \<le> ?\<mu> K * real (?m ^ ?m)"
             proof -
               obtain n where n: "\<And>i. v$i - u$i = 2 * c / 2^n"