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