--- 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