diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Implementation/Proof.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -58,14 +58,14 @@
 notepad
 begin
   {
-    fix x  -- \<open>all potential occurrences of some \<open>x::\<tau>\<close> are fixed\<close>
+    fix x  \<comment> \<open>all potential occurrences of some \<open>x::\<tau>\<close> are fixed\<close>
     {
-      have "x::'a \<equiv> x"  -- \<open>implicit type assignment by concrete occurrence\<close>
+      have "x::'a \<equiv> x"  \<comment> \<open>implicit type assignment by concrete occurrence\<close>
         by (rule reflexive)
     }
-    thm this  -- \<open>result still with fixed type \<open>'a\<close>\<close>
+    thm this  \<comment> \<open>result still with fixed type \<open>'a\<close>\<close>
   }
-  thm this  -- \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
+  thm this  \<comment> \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
 end
 
 text \<open>The Isabelle/Isar proof context manages the details of term