diff -r e9ab4ad7bd15 -r 23307fd33906 src/Doc/Tutorial/Rules/Tacticals.thy
--- a/src/Doc/Tutorial/Rules/Tacticals.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Rules/Tacticals.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -1,6 +1,6 @@
 theory Tacticals imports Main begin
 
-text{*REPEAT*}
+text\<open>REPEAT\<close>
 lemma "\<lbrakk>P\<longrightarrow>Q; Q\<longrightarrow>R; R\<longrightarrow>S; P\<rbrakk> \<Longrightarrow> S"
 apply (drule mp, assumption)
 apply (drule mp, assumption)
@@ -11,32 +11,32 @@
 lemma "\<lbrakk>P\<longrightarrow>Q; Q\<longrightarrow>R; R\<longrightarrow>S; P\<rbrakk> \<Longrightarrow> S"
 by (drule mp, assumption)+
 
-text{*ORELSE with REPEAT*}
+text\<open>ORELSE with REPEAT\<close>
 lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<5\<longrightarrow>P;  Suc x < 5\<rbrakk> \<Longrightarrow> R" 
 by (drule mp, (assumption|arith))+
 
-text{*exercise: what's going on here?*}
+text\<open>exercise: what's going on here?\<close>
 lemma "\<lbrakk>P\<and>Q\<longrightarrow>R; P\<longrightarrow>Q; P\<rbrakk> \<Longrightarrow> R"
 by (drule mp, (intro conjI)?, assumption+)+
 
-text{*defer and prefer*}
+text\<open>defer and prefer\<close>
 
 lemma "hard \<and> (P \<or> ~P) \<and> (Q\<longrightarrow>Q)"
-apply (intro conjI)   --{* @{subgoals[display,indent=0,margin=65]} *}
-defer 1   --{* @{subgoals[display,indent=0,margin=65]} *}
-apply blast+   --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (intro conjI)   \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+defer 1   \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+apply blast+   \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
 oops
 
 lemma "ok1 \<and> ok2 \<and> doubtful"
-apply (intro conjI)   --{* @{subgoals[display,indent=0,margin=65]} *}
-prefer 3   --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (intro conjI)   \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+prefer 3   \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
 oops
 
 lemma "bigsubgoal1 \<and> bigsubgoal2 \<and> bigsubgoal3 \<and> bigsubgoal4 \<and> bigsubgoal5 \<and> bigsubgoal6"
-apply (intro conjI)   --{* @{subgoals[display,indent=0,margin=65]} *}
-txt{* @{subgoals[display,indent=0,margin=65]} 
+apply (intro conjI)   \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+txt\<open>@{subgoals[display,indent=0,margin=65]} 
 A total of 6 subgoals...
-*}
+\<close>
 oops