src/HOL/Analysis/Euclidean_Space.thy

   Inner_Product
   Product_Vector
 begin
 
 
-subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Interlude: Some properties of real sets\<close>
 
 lemma seq_mono_lemma:
   assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
     and "\<forall>n \<ge> m. e n \<le> e m"
   shows "\<forall>n \<ge> m. d n < e m"

   also have "\<dots> = 2 * real DIM('n) * e" by simp
   finally show ?thesis .
 qed
 
 
-subsection%unimportant \<open>Subclass relationships\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Subclass relationships\<close>
 
 instance euclidean_space \<subseteq> perfect_space
 proof
   fix x :: 'a show "\<not> open {x}"
   proof

   qed
 qed
 
 subsection \<open>Class instances\<close>
 
-subsubsection%unimportant \<open>Type \<^typ>\<open>real\<close>\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Type \<^typ>\<open>real\<close>\<close>
 
 instantiation real :: euclidean_space
 begin
 
 definition

 end
 
 lemma DIM_real[simp]: "DIM(real) = 1"
   by simp
 
-subsubsection%unimportant \<open>Type \<^typ>\<open>complex\<close>\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Type \<^typ>\<open>complex\<close>\<close>
 
 instantiation complex :: euclidean_space
 begin
 
 definition Basis_complex_def: "Basis = {1, \<i>}"

   by (simp add: Basis_complex_def)
 
 lemma complex_Basis_i [iff]: "\<i> \<in> Basis"
   by (simp add: Basis_complex_def)
 
-subsubsection%unimportant \<open>Type \<^typ>\<open>'a \<times> 'b\<close>\<close>
+subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Type \<^typ>\<open>'a \<times> 'b\<close>\<close>
 
 instantiation prod :: (real_inner, real_inner) real_inner
 begin
 
 definition inner_prod_def: