src/HOL/Algebra/IntRing.thy

   rewrites "carrier \<Z> = UNIV"
     and "mult \<Z> x y = x * y"
     and "one \<Z> = 1"
     and "pow \<Z> x n = x^n"
 proof -
-  \<comment> "Specification"
+  \<comment> \<open>Specification\<close>
   show "monoid \<Z>" by standard auto
   then interpret int: monoid \<Z> .
 
-  \<comment> "Carrier"
+  \<comment> \<open>Carrier\<close>
   show "carrier \<Z> = UNIV" by simp
 
-  \<comment> "Operations"
+  \<comment> \<open>Operations\<close>
   { fix x y show "mult \<Z> x y = x * y" by simp }
   show "one \<Z> = 1" by simp
   show "pow \<Z> x n = x^n" by (induct n) simp_all
 qed
 
 interpretation int: comm_monoid \<Z>
   rewrites "finprod \<Z> f A = prod f A"
 proof -
-  \<comment> "Specification"
+  \<comment> \<open>Specification\<close>
   show "comm_monoid \<Z>" by standard auto
   then interpret int: comm_monoid \<Z> .
 
-  \<comment> "Operations"
+  \<comment> \<open>Operations\<close>
   { fix x y have "mult \<Z> x y = x * y" by simp }
   note mult = this
   have one: "one \<Z> = 1" by simp
   show "finprod \<Z> f A = prod f A"
     by (induct A rule: infinite_finite_induct, auto)

   rewrites int_carrier_eq: "carrier \<Z> = UNIV"
     and int_zero_eq: "zero \<Z> = 0"
     and int_add_eq: "add \<Z> x y = x + y"
     and int_finsum_eq: "finsum \<Z> f A = sum f A"
 proof -
-  \<comment> "Specification"
+  \<comment> \<open>Specification\<close>
   show "abelian_monoid \<Z>" by standard auto
   then interpret int: abelian_monoid \<Z> .
 
-  \<comment> "Carrier"
+  \<comment> \<open>Carrier\<close>
   show "carrier \<Z> = UNIV" by simp
 
-  \<comment> "Operations"
+  \<comment> \<open>Operations\<close>
   { fix x y show "add \<Z> x y = x + y" by simp }
   note add = this
   show zero: "zero \<Z> = 0"
     by simp
   show "finsum \<Z> f A = sum f A"

     and "add \<Z> x y = x + y"
     and "finsum \<Z> f A = sum f A"
     and int_a_inv_eq: "a_inv \<Z> x = - x"
     and int_a_minus_eq: "a_minus \<Z> x y = x - y"
 proof -
-  \<comment> "Specification"
+  \<comment> \<open>Specification\<close>
   show "abelian_group \<Z>"
   proof (rule abelian_groupI)
     fix x
     assume "x \<in> carrier \<Z>"
     then show "\<exists>y \<in> carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
       by simp arith
   qed auto
   then interpret int: abelian_group \<Z> .
-  \<comment> "Operations"
+  \<comment> \<open>Operations\<close>
   { fix x y have "add \<Z> x y = x + y" by simp }
   note add = this
   have zero: "zero \<Z> = 0" by simp
   {
     fix x