diff -r 2e48182cc82c -r cf58b5b794b2 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Records.thy	Sat Dec 26 15:59:27 2015 +0100
@@ -75,19 +75,19 @@
 text \<open>\medskip Equality of records.\<close>
 
 lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
-  -- "introduction of concrete record equality"
+  \<comment> "introduction of concrete record equality"
   by simp
 
 lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
-  -- "elimination of concrete record equality"
+  \<comment> "elimination of concrete record equality"
   by simp
 
 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
-  -- "introduction of abstract record equality"
+  \<comment> "introduction of abstract record equality"
   by simp
 
 lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
-  -- "elimination of abstract record equality (manual proof)"
+  \<comment> "elimination of abstract record equality (manual proof)"
 proof -
   assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
   then have "xpos ?lhs = xpos ?rhs" by simp
@@ -149,7 +149,7 @@
   where "foo5 = getX (| xpos = 1, ypos = 0 |)"
 
 
-text \<open>\medskip Manipulating the ``@{text "..."}'' (more) part.\<close>
+text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close>
 
 definition incX :: "'a point_scheme => 'a point_scheme"
   where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
@@ -188,7 +188,7 @@
 
 
 text \<open>
- Functions on @{text point} schemes work for @{text cpoints} as well.
+ Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.
 \<close>
 
 definition foo10 :: nat