src/FOL/ex/Locale_Test/Locale_Test1.thy

 lemma linv: "inv(x) ** x = one"
   unfolding one_def inv_def by (rule glob_linv)
 
 end
 
-sublocale lgrp < "def"?: dgrp
+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 .
   \<comment> Unit