src/FOL/ex/Locale_Test/Locale_Test1.thy

 print_locale! perturbation thm perturbation_def
 
 locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
 print_locale! pert_hom thm pert_hom_def
 
-text \<open>Alternative expression, obtaining nicer names in @{text "semi f"}.\<close>
+text \<open>Alternative expression, obtaining nicer names in \<open>semi f\<close>.\<close>
 locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
 print_locale! pert_hom' thm pert_hom'_def
 
 
 section \<open>Syntax declarations\<close>

 sublocale lgrp < "def"?: dgrp
   rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
 proof -
   show "dgrp(prod)" by unfold_locales
   from this interpret d: dgrp .
-  -- Unit
+  \<comment> Unit
   have "dgrp.one(prod) = glob_one(prod)" by (rule d.one_def)
   also have "... = glob_one(prod) ** one" by (simp add: rone)
   also have "... = one" by (simp add: glob_lone)
   finally show "dgrp.one(prod) = one" .
-  -- Inverse
+  \<comment> Inverse
   then have "dgrp.inv(prod, x) ** x = inv(x) ** x" by (simp add: glob_linv d.linv linv)
   then show "dgrp.inv(prod, x) = inv(x)" by (simp add: rcancel)
 qed
 
 print_locale! lgrp