diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Thu May 26 17:51:22 2016 +0200
@@ -84,28 +84,28 @@
 text \<open>The quotient is a ring\<close>
 lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
 apply (rule ringI)
-   --\<open>abelian group\<close>
+   \<comment>\<open>abelian group\<close>
    apply (rule comm_group_abelian_groupI)
    apply (simp add: FactRing_def)
    apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
-  --\<open>mult monoid\<close>
+  \<comment>\<open>mult monoid\<close>
   apply (rule monoidI)
       apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def
              a_r_coset_def[symmetric])
-      --\<open>mult closed\<close>
+      \<comment>\<open>mult closed\<close>
       apply (clarify)
       apply (simp add: rcoset_mult_add, fast)
-     --\<open>mult @{text one_closed}\<close>
+     \<comment>\<open>mult \<open>one_closed\<close>\<close>
      apply force
-    --\<open>mult assoc\<close>
+    \<comment>\<open>mult assoc\<close>
     apply clarify
     apply (simp add: rcoset_mult_add m_assoc)
-   --\<open>mult one\<close>
+   \<comment>\<open>mult one\<close>
    apply clarify
    apply (simp add: rcoset_mult_add)
   apply clarify
   apply (simp add: rcoset_mult_add)
- --\<open>distr\<close>
+ \<comment>\<open>distr\<close>
  apply clarify
  apply (simp add: rcoset_mult_add a_rcos_sum l_distr)
 apply clarify
@@ -225,7 +225,7 @@
      apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp)
      apply (simp add: rcoset_mult_add) defer 1
   proof (rule ccontr, simp)
-    --\<open>Quotient is not empty\<close>
+    \<comment>\<open>Quotient is not empty\<close>
     assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
     then have II1: "I = I +> \<one>" by (simp add: FactRing_def)
     from a_rcos_self[OF one_closed] have "\<one> \<in> I"
@@ -233,11 +233,11 @@
     then have "I = carrier R" by (rule one_imp_carrier)
     with I_notcarr show False by simp
   next
-    --\<open>Existence of Inverse\<close>
+    \<comment>\<open>Existence of Inverse\<close>
     fix a
     assume IanI: "I +> a \<noteq> I" and acarr: "a \<in> carrier R"
 
-    --\<open>Helper ideal @{text "J"}\<close>
+    \<comment>\<open>Helper ideal \<open>J\<close>\<close>
     define J :: "'a set" where "J = (carrier R #> a) <+> I"
     have idealJ: "ideal J R"
       apply (unfold J_def, rule add_ideals)
@@ -245,7 +245,7 @@
       apply (rule is_ideal)
       done
 
-    --\<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
+    \<comment>\<open>Showing @{term "J"} not smaller than @{term "I"}\<close>
     have IinJ: "I \<subseteq> J"
     proof (rule, simp add: J_def r_coset_def set_add_defs)
       fix x
@@ -256,7 +256,7 @@
       with Zcarr and xI show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
     qed
 
-    --\<open>Showing @{term "J \<noteq> I"}\<close>
+    \<comment>\<open>Showing @{term "J \<noteq> I"}\<close>
     have anI: "a \<notin> I"
     proof (rule ccontr, simp)
       assume "a \<in> I"
@@ -274,7 +274,7 @@
 
     from aJ and anI have JnI: "J \<noteq> I" by fast
 
-    --\<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
+    \<comment>\<open>Deducing @{term "J = carrier R"} because @{term "I"} is maximal\<close>
     from idealJ and IinJ have "J = I \<or> J = carrier R"
     proof (rule I_maximal, unfold J_def)
       have "carrier R #> a \<subseteq> carrier R"
@@ -285,7 +285,7 @@
 
     with JnI have Jcarr: "J = carrier R" by simp
 
-    --\<open>Calculating an inverse for @{term "a"}\<close>
+    \<comment>\<open>Calculating an inverse for @{term "a"}\<close>
     from one_closed[folded Jcarr]
     have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
       by (simp add: J_def r_coset_def set_add_defs)
@@ -294,7 +294,7 @@
     from one and rcarr and acarr and iI[THEN a_Hcarr]
     have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
 
-    --\<open>Lifting to cosets\<close>
+    \<comment>\<open>Lifting to cosets\<close>
     from iI have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
       by (intro a_rcosI, simp, intro a_subset, simp)
     with rai1 have "a \<otimes> r \<in> I +> \<one>" by simp