--- a/src/HOL/Isar_Examples/Structured_Statements.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy Mon Dec 07 10:38:04 2015 +0100
@@ -152,9 +152,9 @@
have C
proof -
- show ?thesis when "A x" (is ?A) for x :: 'a -- \<open>abstract @{term x}\<close>
+ show ?thesis when "A x" (is ?A) for x :: 'a \<comment> \<open>abstract @{term x}\<close>
using that sorry
- show "?A a" -- \<open>concrete @{term a}\<close>
+ show "?A a" \<comment> \<open>concrete @{term a}\<close>
sorry
qed
end