src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy

           and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
           and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
           unfolding H'_def sum_def lin_def by blast
         
         have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
-        proof (rule decomp_H') txt_raw \<open>\label{decomp-H-use}\<close>
+        proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>
           from HE y1 y2 show "y1 + y2 \<in> H"
             by (rule subspace.add_closed)
           from x0 and HE y y1 y2
           have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
           with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"