src/HOL/ex/Dedekind_Real.thy

 
 subsection\<open>Properties of Addition\<close>
 
 lemma preal_add_commute: "(x::preal) + y = y + x"
   unfolding preal_add_def add_set_def
-  by (metis (no_types, hide_lams) add.commute)
+  by (metis (no_types, opaque_lifting) add.commute)
 
 text\<open>Lemmas for proving that addition of two positive reals gives
  a positive real\<close>
 
 lemma mem_add_set:

 
 text\<open>Proofs essentially same as for addition\<close>
 
 lemma preal_mult_commute: "(x::preal) * y = y * x"
   unfolding preal_mult_def mult_set_def
-  by (metis (no_types, hide_lams) mult.commute)
+  by (metis (no_types, opaque_lifting) mult.commute)
 
 text\<open>Multiplication of two positive reals gives a positive real.\<close>
 
 lemma mem_mult_set:
   assumes "cut A" "cut B"

 qed
 
 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
   apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   apply (simp add: mult_set_def)
-  apply (metis (no_types, hide_lams) ab_semigroup_mult_class.mult_ac(1))
+  apply (metis (no_types, opaque_lifting) ab_semigroup_mult_class.mult_ac(1))
   done
 
 instance preal :: ab_semigroup_mult
 proof
   fix a b c :: preal

 
 lemma real_mult_congruent2_lemma:
      "!!(x1::preal). \<lbrakk>x1 + y2 = x2 + y1\<rbrakk> \<Longrightarrow>
           x * x1 + y * y1 + (x * y2 + y * x2) =
           x * x2 + y * y2 + (x * y1 + y * x1)"
-  by (metis (no_types, hide_lams) add.left_commute preal_add_commute preal_add_mult_distrib2)
+  by (metis (no_types, opaque_lifting) add.left_commute preal_add_commute preal_add_mult_distrib2)
 
 lemma real_mult_congruent2:
   "(\<lambda>p1 p2.
         (\<lambda>(x1,y1). (\<lambda>(x2,y2). 
           { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)