src/HOL/Analysis/Winding_Numbers.thy

     by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
   from u(1) show "z \<in> closed_segment a b" using assms
     by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
 qed
 
-definition%important rectpath where
+definition\<^marker>\<open>tag important\<close> rectpath where
   "rectpath a1 a3 = (let a2 = Complex (Re a3) (Im a1); a4 = Complex (Re a1) (Im a3)
                       in linepath a1 a2 +++ linepath a2 a3 +++ linepath a3 a4 +++ linepath a4 a1)"
 
 lemma path_rectpath [simp, intro]: "path (rectpath a b)"
   by (simp add: Let_def rectpath_def)

   shows   "winding_number (rectpath a1 a3) z = 0"
   using assms by (intro winding_number_zero_outside[OF _ _ _ assms(3)]
                      path_image_rectpath_subset_cbox) simp_all
 
 text\<open>A per-function version for continuous logs, a kind of monodromy\<close>
-proposition%unimportant winding_number_compose_exp:
+proposition\<^marker>\<open>tag unimportant\<close> winding_number_compose_exp:
   assumes "path p"
   shows "winding_number (exp \<circ> p) 0 = (pathfinish p - pathstart p) / (2 * of_real pi * \<i>)"
 proof -
   obtain e where "0 < e" and e: "\<And>t. t \<in> {0..1} \<Longrightarrow> e \<le> norm(exp(p t))"
   proof

       using \<open>g 0 = p 0\<close> \<open>g 1 = p 1\<close> by auto
   qed
   finally show ?thesis .
 qed
 
-subsection%unimportant \<open>The winding number defines a continuous logarithm for the path itself\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>The winding number defines a continuous logarithm for the path itself\<close>
 
 lemma winding_number_as_continuous_log:
   assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
   obtains q where "path q"
                   "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"