
diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Tue May 14 17:10:47 2019 +0200
@@ -2,9 +2,9 @@
 imports Base First_Steps
 begin
 
-chapter {* Tactical Reasoning\label{chp:tactical} *}
-
-text {*
+chapter \<open>Tactical Reasoning\label{chp:tactical}\<close>
+
+text \<open>
    \begin{flushright}
   {\em
   ``The first thing I would say is that when you write a program, think of\\ 
@@ -26,14 +26,14 @@
   modified in a sequence of proof steps until all of them are discharged.
   In this chapter we explain how to implement simple tactics and how to combine them using
   tactic combinators. We also describe the simplifier, simprocs and conversions.
-*}
-
-section {* Basics of Reasoning with Tactics\label{sec:basictactics}*}
-
-text {*
+\<close>
+
+section \<open>Basics of Reasoning with Tactics\label{sec:basictactics}\<close>
+
+text \<open>
   To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 
   into ML. Suppose the following proof.
-*}
+\<close>
 
 lemma disj_swap: 
   shows "P \<or> Q \<Longrightarrow> Q \<or> P"
@@ -44,7 +44,7 @@
 apply(assumption)
 done
 
-text {*
+text \<open>
   This proof translates to the following ML-code.
   
 @{ML_response_fake [display,gray]
@@ -65,12 +65,11 @@
   function some assumptions in the third argument (there are no assumption in
   the proof at hand). The second argument stands for a list of variables
   (given as strings). This list contains the variables that will be turned
-  into schematic variables once the goal is proved (in our case @{text P} and
-  @{text Q}). The last argument is the tactic that proves the goal. This
+  into schematic variables once the goal is proved (in our case \<open>P\<close> and
+  \<open>Q\<close>). The last argument is the tactic that proves the goal. This
   tactic can make use of the local assumptions (there are none in this
   example). The tactics @{ML_ind eresolve_tac in Tactic}, @{ML_ind resolve_tac in Tactic} and
-  @{ML_ind assume_tac in Tactic} in the code above correspond roughly to @{text
-  erule}, @{text rule} and @{text assumption}, respectively. The combinator
+  @{ML_ind assume_tac in Tactic} in the code above correspond roughly to \<open>erule\<close>, \<open>rule\<close> and \<open>assumption\<close>, respectively. The combinator
   @{ML THEN} strings the tactics together.
 
   TBD: Write something about @{ML_ind prove_common in Goal}.
@@ -89,64 +88,64 @@
   \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}}
   During the development of automatic proof procedures, you will often find it
   necessary to test a tactic on examples. This can be conveniently done with
-  the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
+  the command \isacommand{apply}\<open>(tactic \<verbopen> \<dots> \<verbclose>)\<close>. 
   Consider the following sequence of tactics
 
-*}
-
-ML %grayML{*fun foo_tac ctxt = 
+\<close>
+
+ML %grayML\<open>fun foo_tac ctxt = 
       (eresolve_tac ctxt [@{thm disjE}] 1
        THEN resolve_tac  ctxt [@{thm disjI2}] 1
        THEN assume_tac  ctxt 1
        THEN resolve_tac ctxt [@{thm disjI1}] 1
-       THEN assume_tac  ctxt 1)*}
-
-text {* and the Isabelle proof: *}
+       THEN assume_tac  ctxt 1)\<close>
+
+text \<open>and the Isabelle proof:\<close>
 
 lemma 
   shows "P \<or> Q \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac @{context} *})
+apply(tactic \<open>foo_tac @{context}\<close>)
 done
 
-text {*
-  By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the 
+text \<open>
+  By using \<open>tactic \<verbopen> \<dots> \<verbclose>\<close> you can call from the 
   user-level of Isabelle the tactic @{ML foo_tac} or 
   any other function that returns a tactic. There are some goal transformations
-  that are performed by @{text "tactic"}. They can be avoided by using 
-  @{text "raw_tactic"} instead.
+  that are performed by \<open>tactic\<close>. They can be avoided by using 
+  \<open>raw_tactic\<close> instead.
 
   The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
   together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}
   has a hard-coded number that stands for the subgoal analysed by the
-  tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
+  tactic (\<open>1\<close> stands for the first, or top-most, subgoal). This hard-coding
   of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, 
   you can write
-*}
-
-ML %grayML{*fun foo_tac' ctxt = 
+\<close>
+
+ML %grayML\<open>fun foo_tac' ctxt = 
       (eresolve_tac ctxt [@{thm disjE}] 
        THEN' resolve_tac ctxt [@{thm disjI2}] 
        THEN' assume_tac ctxt 
        THEN' resolve_tac ctxt [@{thm disjI1}] 
-       THEN' assume_tac ctxt)*}text_raw{*\label{tac:footacprime}*}
-
-text {* 
+       THEN' assume_tac ctxt)\<close>text_raw\<open>\label{tac:footacprime}\<close>
+
+text \<open>
   where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in
   Tactical}. (For most combinators that combine tactics---@{ML THEN} is only
   one such combinator---a ``primed'' version exists.)  With @{ML foo_tac'} you
   can give the number for the subgoal explicitly when the tactic is called. So
   in the next proof you can first discharge the second subgoal, and
   then the first.
-*}
+\<close>
 
 lemma 
   shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
   and   "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
-apply(tactic {* foo_tac' @{context} 2 *})
-apply(tactic {* foo_tac' @{context} 1 *})
+apply(tactic \<open>foo_tac' @{context} 2\<close>)
+apply(tactic \<open>foo_tac' @{context} 1\<close>)
 done
 
-text {*
+text \<open>
   This kind of addressing is more difficult to achieve when the goal is 
   hard-coded inside the tactic. 
 
@@ -158,38 +157,38 @@
 
 
   \begin{isabelle}
-  @{text "*** empty result sequence -- proof command failed"}\\
-  @{text "*** At command \"apply\"."}
+  \<open>*** empty result sequence -- proof command failed\<close>\\
+  \<open>*** At command "apply".\<close>
   \end{isabelle}
 
   This means they failed. The reason for this error message is that tactics
   are functions mapping a goal state to a (lazy) sequence of successor
   states. Hence the type of a tactic is:
-*}
+\<close>
   
-ML %grayML{*type tactic = thm -> thm Seq.seq*}
-
-text {*
+ML %grayML\<open>type tactic = thm -> thm Seq.seq\<close>
+
+text \<open>
   By convention, if a tactic fails, then it should return the empty sequence. 
   Therefore, your own tactics should not raise exceptions 
   willy-nilly; only in very grave failure situations should a tactic raise the
-  exception @{text THM}.
+  exception \<open>THM\<close>.
 
   The simplest tactics are @{ML_ind no_tac in Tactical} and 
   @{ML_ind all_tac in Tactical}. The first returns the empty sequence and 
   is defined as
-*}
-
-ML %grayML{*fun no_tac thm = Seq.empty*}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun no_tac thm = Seq.empty\<close>
+
+text \<open>
   which means @{ML no_tac} always fails. The second returns the given theorem wrapped 
   in a single member sequence; it is defined as
-*}
-
-ML %grayML{*fun all_tac thm = Seq.single thm*}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun all_tac thm = Seq.single thm\<close>
+
+text \<open>
   which means @{ML all_tac} always succeeds, but also does not make any progress 
   with the proof.
 
@@ -197,16 +196,16 @@
   of Isabelle when using the command \isacommand{back}. For instance in the 
   following proof there are two possibilities for how to apply 
   @{ML foo_tac'}: either using the first assumption or the second.
-*}
+\<close>
 
 lemma 
   shows "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac' @{context} 1 *})
+apply(tactic \<open>foo_tac' @{context} 1\<close>)
 back
 done
 
 
-text {*
+text \<open>
   By using \isacommand{back}, we construct the proof that uses the
   second assumption. While in the proof above, it does not really matter which 
   assumption is used, in more interesting cases provability might depend
@@ -225,16 +224,16 @@
   goal state is indeed a theorem. To shed more light on this,
   let us modify the code of @{ML all_tac} to obtain the following
   tactic
-*}
-
-ML %grayML{*fun my_print_tac ctxt thm =
+\<close>
+
+ML %grayML\<open>fun my_print_tac ctxt thm =
 let
   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
 in 
   Seq.single thm
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   which prints out the given theorem (using the string-function defined in
   Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
   tactic we are in the position to inspect every goal state in a proof. For
@@ -245,30 +244,29 @@
 
   where @{term C} is the goal to be proved and the @{term "A\<^sub>i"} are
   the subgoals. So after setting up the lemma, the goal state is always of the
-  form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
-  "#C"}. Since the goal @{term C} can potentially be an implication, there is a
+  form \<open>C \<Longrightarrow> #C\<close>; when the proof is finished we are left with \<open>#C\<close>. Since the goal @{term C} can potentially be an implication, there is a
   ``protector'' wrapped around it (the wrapper is the outermost constant
-  @{text "Const (\"Pure.prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
-  as a @{text #}). This wrapper prevents that premises of @{text C} are
+  \<open>Const ("Pure.prop", bool \<Rightarrow> bool)\<close>; in the figure we make it visible
+  as a \<open>#\<close>). This wrapper prevents that premises of \<open>C\<close> are
   misinterpreted as open subgoals. While tactics can operate on the subgoals
-  (the @{text "A\<^sub>i"} above), they are expected to leave the conclusion
+  (the \<open>A\<^sub>i\<close> above), they are expected to leave the conclusion
   @{term C} intact, with the exception of possibly instantiating schematic
   variables. This instantiations of schematic variables can be observed 
   on the user level. Have a look at the following definition and proof.
-*}
-
-text_raw {*
+\<close>
+
+text_raw \<open>
   \begin{figure}[p]
   \begin{boxedminipage}{\textwidth}
   \begin{isabelle}
-*}
+\<close>
 notation (output) "Pure.prop"  ("#_" [1000] 1000)
 
 lemma 
   shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
-apply(tactic {* my_print_tac @{context} *})
-
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>my_print_tac @{context}\<close>)
+
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]} 
       \end{minipage}\medskip      
 
@@ -279,12 +277,12 @@
       @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
-*}
+\<close>
 
 apply(rule conjI)
-apply(tactic {* my_print_tac @{context} *})
-
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>my_print_tac @{context}\<close>)
+
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]} 
       \end{minipage}\medskip
 
@@ -295,12 +293,12 @@
       @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
-*}
+\<close>
 
 apply(assumption)
-apply(tactic {* my_print_tac @{context} *})
-
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>my_print_tac @{context}\<close>)
+
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]} 
       \end{minipage}\medskip
 
@@ -311,12 +309,12 @@
       @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip
-*}
+\<close>
 
 apply(assumption)
-apply(tactic {* my_print_tac @{context} *})
-
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>my_print_tac @{context}\<close>)
+
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]} 
       \end{minipage}\medskip 
   
@@ -327,21 +325,21 @@
       @{raw_goal_state}
       \end{tabular}}
       \end{minipage}\medskip   
-   *}
+\<close>
 (*<*)oops(*>*)
-text_raw {*  
+text_raw \<open>
   \end{isabelle}
   \end{boxedminipage}
   \caption{The figure shows an Isabelle snippet of a proof where each
   intermediate goal state is printed by the Isabelle system and by @{ML
   my_print_tac}. The latter shows the goal state as represented internally
   (highlighted boxes). This tactic shows that every goal state in Isabelle is
-  represented by a theorem: when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow>
-  A \<and> B"}} the theorem is @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when
-  you finish the proof the theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and>
-  B)"}.\label{fig:goalstates}}
+  represented by a theorem: when you start the proof of \mbox{\<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow>
+  A \<and> B\<close>} the theorem is \<open>(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)\<close>; when
+  you finish the proof the theorem is \<open>#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and>
+  B)\<close>.\label{fig:goalstates}}
   \end{figure}
-*}
+\<close>
 
 definition 
   EQ_TRUE 
@@ -353,17 +351,17 @@
 unfolding EQ_TRUE_def
 by (rule refl)
 
-text {*
+text \<open>
   By using \isacommand{schematic\_lemma} it is possible to prove lemmas including
-  meta-variables on the user level. However, the proved theorem is not @{text "EQ_TRUE ?X"}, 
+  meta-variables on the user level. However, the proved theorem is not \<open>EQ_TRUE ?X\<close>, 
   as one might expect, but @{thm test}. We can test this with:
 
   \begin{isabelle}
   \isacommand{thm}~@{thm [source] test}\\
-  @{text ">"}~@{thm test}
+  \<open>>\<close>~@{thm test}
   \end{isabelle}
  
-  The reason for this result is that the schematic variable @{text "?X"} 
+  The reason for this result is that the schematic variable \<open>?X\<close> 
   is instantiated inside the proof to be @{term True} and then the 
   instantiation propagated to the ``outside''.
 
@@ -371,116 +369,115 @@
   For more information about the internals of goals see \isccite{sec:tactical-goals}.
   \end{readmore}
 
-*}
-
-
-section {* Simple Tactics\label{sec:simpletacs} *}
-
-text {*
+\<close>
+
+
+section \<open>Simple Tactics\label{sec:simpletacs}\<close>
+
+text \<open>
   In this section we will introduce more of the simple tactics in Isabelle. The 
   first one is @{ML_ind print_tac in Tactical}, which is quite useful 
   for low-level debugging of tactics. It just prints out a message and the current 
   goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 
   as the user would see it.  For example, processing the proof
-*}
+\<close>
  
 lemma 
   shows "False \<Longrightarrow> True"
-apply(tactic {* print_tac @{context} "foo message" *})
-txt{*gives:
+apply(tactic \<open>print_tac @{context} "foo message"\<close>)
+txt\<open>gives:
      \begin{isabelle}
-     @{text "foo message"}\\[3mm] 
+     \<open>foo message\<close>\\[3mm] 
      @{prop "False \<Longrightarrow> True"}\\
-     @{text " 1. False \<Longrightarrow> True"}\\
+     \<open> 1. False \<Longrightarrow> True\<close>\\
      \end{isabelle}
-   *}
+\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   A simple tactic for easy discharge of any proof obligations, even difficult ones, is 
   @{ML_ind cheat_tac in Skip_Proof} in the structure @{ML_struct Skip_Proof}. 
   This tactic corresponds to the Isabelle command \isacommand{sorry} and is 
   sometimes useful during the development of tactics.
-*}
+\<close>
 
 lemma 
   shows "False" and "Goldbach_conjecture"  
-apply(tactic {* Skip_Proof.cheat_tac @{context} 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>Skip_Proof.cheat_tac @{context} 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Another simple tactic is the function @{ML_ind assume_tac in Tactic}, which, as shown 
   earlier, corresponds to the assumption method.
-*}
+\<close>
 
 lemma 
   shows "P \<Longrightarrow> P"
-apply(tactic {* assume_tac @{context} 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>assume_tac @{context} 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Similarly, @{ML_ind resolve_tac in Tactic}, @{ML_ind dresolve_tac in Tactic}, @{ML_ind eresolve_tac
-  in Tactic} and @{ML_ind forward_tac in Tactic} correspond (roughly) to @{text
-  rule}, @{text drule}, @{text erule} and @{text frule}, respectively. Each of
+  in Tactic} and @{ML_ind forward_tac in Tactic} correspond (roughly) to \<open>rule\<close>, \<open>drule\<close>, \<open>erule\<close> and \<open>frule\<close>, respectively. Each of
   them takes a theorem as argument and attempts to apply it to a goal. Below
   are three self-explanatory examples.
-*}
+\<close>
 
 lemma 
   shows "P \<and> Q"
-apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>resolve_tac @{context} [@{thm conjI}] 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
 lemma 
   shows "P \<and> Q \<Longrightarrow> False"
-apply(tactic {* eresolve_tac @{context} [@{thm conjE}] 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>eresolve_tac @{context} [@{thm conjE}] 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
 lemma 
   shows "False \<and> True \<Longrightarrow> False"
-apply(tactic {* dresolve_tac @{context} [@{thm conjunct2}] 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>dresolve_tac @{context} [@{thm conjunct2}] 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   The function @{ML_ind resolve_tac in Tactic} 
   expects a list of theorems as argument. From this list it will apply the
   first applicable theorem (later theorems that are also applicable can be
   explored via the lazy sequences mechanism). Given the code
-*}
-
-ML %grayML{*fun resolve_xmp_tac ctxt = resolve_tac ctxt [@{thm impI}, @{thm conjI}]*}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun resolve_xmp_tac ctxt = resolve_tac ctxt [@{thm impI}, @{thm conjI}]\<close>
+
+text \<open>
   an example for @{ML resolve_tac} is the following proof where first an outermost 
   implication is analysed and then an outermost conjunction.
-*}
+\<close>
 
 lemma 
   shows "C \<longrightarrow> (A \<and> B)" 
   and   "(A \<longrightarrow> B) \<and> C"
-apply(tactic {* resolve_xmp_tac @{context} 1 *})
-apply(tactic {* resolve_xmp_tac @{context} 2 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>resolve_xmp_tac @{context} 1\<close>)
+apply(tactic \<open>resolve_xmp_tac @{context} 2\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]} 
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {* 
+text \<open>
   Similar versions taking a list of theorems exist for the tactics 
    @{ML_ind dresolve_tac in Tactic},  
   @{ML_ind eresolve_tac in Tactic} and so on.
@@ -489,20 +486,20 @@
   list of theorems into the assumptions of the current goal state. Below we
   will insert the definitions for the constants @{term True} and @{term
   False}. So
-*}
+\<close>
 
 lemma 
   shows "True \<noteq> False"
-apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
-txt{*produces the goal state
+apply(tactic \<open>cut_facts_tac [@{thm True_def}, @{thm False_def}] 1\<close>)
+txt\<open>produces the goal state
      \begin{isabelle}
      @{subgoals [display]} 
-     \end{isabelle}*}
+     \end{isabelle}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Often proofs on the ML-level involve elaborate operations on assumptions and 
-  @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
+  \<open>\<And>\<close>-quantified variables. To do such operations using the basic tactics 
   shown so far is very unwieldy and brittle. Some convenience and
   safety is provided by the functions @{ML_ind FOCUS in Subgoal} and 
   @{ML_ind SUBPROOF in Subgoal}. These tactics fix the parameters 
@@ -510,16 +507,16 @@
   To see what happens, suppose the function defined in Figure~\ref{fig:sptac}, which
   takes a record and just prints out the contents of this record. Then consider
   the proof:
-*}
-
-
-text_raw{*
+\<close>
+
+
+text_raw\<open>
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}
-*}
-
-ML %grayML{*fun foc_tac {context, params, prems, asms, concl, schematics} = 
+\<close>
+
+ML %grayML\<open>fun foc_tac {context, params, prems, asms, concl, schematics} = 
 let 
   fun assgn1 f1 f2 xs =
     let
@@ -538,9 +535,9 @@
      ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))]
 in
   tracing (Pretty.string_of (Pretty.chunks pps)); all_tac 
-end*}
-
-text_raw{*
+end\<close>
+
+text_raw\<open>
 \end{isabelle}
 \end{minipage}
 \caption{A function that prints out the various parameters provided by 
@@ -548,57 +545,57 @@
   in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s 
   and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
-*}
+\<close>
 
 schematic_goal
   shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
-apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
-
-txt {*
+apply(tactic \<open>Subgoal.FOCUS foc_tac @{context} 1\<close>)
+
+txt \<open>
   The tactic produces the following printout:
 
   \begin{quote}\small
   \begin{tabular}{ll}
-  params:      & @{text "x:= x"}, @{text "y:= y"}\\
+  params:      & \<open>x:= x\<close>, \<open>y:= y\<close>\\
   assumptions: & @{term "A x y"}\\
   conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
   premises:    & @{term "A x y"}\\
-  schematics:  & @{text "?z:=z"}
+  schematics:  & \<open>?z:=z\<close>
   \end{tabular}
   \end{quote}
 
-  The @{text params} and @{text schematics} stand for list of pairs where the
-  left-hand side of @{text ":="} is replaced by the right-hand side inside the
+  The \<open>params\<close> and \<open>schematics\<close> stand for list of pairs where the
+  left-hand side of \<open>:=\<close> is replaced by the right-hand side inside the
   tactic.  Notice that in the actual output the variables @{term x} and @{term
   y} have a brown colour. Although they are parameters in the original goal,
   they are fixed inside the tactic. By convention these fixed variables are
-  printed in brown colour.  Similarly the schematic variable @{text ?z}. The
+  printed in brown colour.  Similarly the schematic variable \<open>?z\<close>. The
   assumption, or premise, @{prop "A x y"} is bound as @{ML_type cterm} to the
-  record-variable @{text asms}, but also as @{ML_type thm} to @{text prems}.
-
-  If we continue the proof script by applying the @{text impI}-rule
-*}
+  record-variable \<open>asms\<close>, but also as @{ML_type thm} to \<open>prems\<close>.
+
+  If we continue the proof script by applying the \<open>impI\<close>-rule
+\<close>
 
 apply(rule impI)
-apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
-
-txt {*
+apply(tactic \<open>Subgoal.FOCUS foc_tac @{context} 1\<close>)
+
+txt \<open>
   then the tactic prints out: 
 
   \begin{quote}\small
   \begin{tabular}{ll}
-  params:      & @{text "x:= x"}, @{text "y:= y"}\\
+  params:      & \<open>x:= x\<close>, \<open>y:= y\<close>\\
   assumptions: & @{term "A x y"}, @{term "B y x"}\\
   conclusion:  & @{term "C (z y) x"}\\
   premises:    & @{term "A x y"}, @{term "B y x"}\\
-  schematics:  & @{text "?z:=z"}
+  schematics:  & \<open>?z:=z\<close>
   \end{tabular}
   \end{quote}
-*}
+\<close>
 (*<*)oops(*>*)
 
-text {*
-  Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
+text \<open>
+  Now also @{term "B y x"} is an assumption bound to \<open>asms\<close> and \<open>prems\<close>.
 
   One difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal}
   is that the former expects that the goal is solved completely, which the
@@ -609,43 +606,43 @@
   state where there is only a conclusion. This means the tactics @{ML dresolve_tac} and 
   the like are of no use for manipulating the goal state. The assumptions inside 
   @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are given as cterms and theorems in 
-  the arguments @{text "asms"} and @{text "prems"}, respectively. This 
+  the arguments \<open>asms\<close> and \<open>prems\<close>, respectively. This 
   means we can apply them using the usual assumption tactics. With this you can 
   for example easily implement a tactic that behaves almost like @{ML assume_tac}:
-*}
-
-ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, context, ...} => resolve_tac context prems 1)*}
-
-text {*
+\<close>
+
+ML %grayML\<open>val atac' = Subgoal.FOCUS (fn {prems, context, ...} => resolve_tac context prems 1)\<close>
+
+text \<open>
   If you apply @{ML atac'} to the next lemma
-*}
+\<close>
 
 lemma 
   shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
-apply(tactic {* atac' @{context} 1 *})
-txt{* it will produce
-      @{subgoals [display]} *}
+apply(tactic \<open>atac' @{context} 1\<close>)
+txt\<open>it will produce
+      @{subgoals [display]}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Notice that @{ML atac'} inside @{ML FOCUS in Subgoal} calls @{ML
-  resolve_tac} with the subgoal number @{text "1"} and also the outer call to
-  @{ML FOCUS in Subgoal} in the \isacommand{apply}-step uses @{text "1"}. This
+  resolve_tac} with the subgoal number \<open>1\<close> and also the outer call to
+  @{ML FOCUS in Subgoal} in the \isacommand{apply}-step uses \<open>1\<close>. This
   is another advantage of @{ML FOCUS in Subgoal} and @{ML SUBPROOF}: the
   addressing inside it is completely local to the tactic inside the
   subproof. It is therefore possible to also apply @{ML atac'} to the second
   goal by just writing:
 
-*}
+\<close>
 
 lemma 
   shows "True" 
   and   "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
-apply(tactic {* atac' @{context} 2 *})
+apply(tactic \<open>atac' @{context} 2\<close>)
 apply(rule TrueI)
 done
 
-text {*
+text \<open>
   To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather
   convenient, but can impose a considerable run-time penalty in automatic
   proofs. If speed is of the essence, then maybe the two lower level combinators 
@@ -665,9 +662,9 @@
   cterm}). With them you can implement a tactic that applies a rule according
   to the topmost logic connective in the subgoal (to illustrate this we only
   analyse a few connectives). The code of the tactic is as follows.
-*}
-
-ML %linenosgray{*fun select_tac ctxt (t, i) =
+\<close>
+
+ML %linenosgray\<open>fun select_tac ctxt (t, i) =
   case t of
      @{term "Trueprop"} $ t' => select_tac ctxt (t', i)
    | @{term "(\<Longrightarrow>)"} $ _ $ t' => select_tac ctxt (t', i)
@@ -675,15 +672,15 @@
    | @{term "(\<longrightarrow>)"} $ _ $ _ => resolve_tac ctxt [@{thm impI}] i
    | @{term "Not"} $ _ => resolve_tac ctxt [@{thm notI}] i
    | Const (@{const_name "All"}, _) $ _ => resolve_tac ctxt [@{thm allI}] i
-   | _ => all_tac*}text_raw{*\label{tac:selecttac}*}
-
-text {*
+   | _ => all_tac\<close>text_raw\<open>\label{tac:selecttac}\<close>
+
+text \<open>
   The input of the function is a term representing the subgoal and a number
   specifying the subgoal of interest. In Line 3 you need to descend under the
   outermost @{term "Trueprop"} in order to get to the connective you like to
   analyse. Otherwise goals like @{prop "A \<and> B"} are not properly
   analysed. Similarly with meta-implications in the next line.  While for the
-  first five patterns we can use the @{text "@term"}-antiquotation to
+  first five patterns we can use the \<open>@term\<close>-antiquotation to
   construct the patterns, the pattern in Line 8 cannot be constructed in this
   way. The reason is that an antiquotation would fix the type of the
   quantified variable. So you really have to construct this pattern using the
@@ -695,36 +692,36 @@
 
 
   Let us now see how to apply this tactic. Consider the four goals:
-*}
+\<close>
 
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
-apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
-apply(tactic {* SUBGOAL (select_tac @{context}) 2 *})
-apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 4\<close>)
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 3\<close>)
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 2\<close>)
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]}
-      \end{minipage} *}
+      \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   where in all but the last the tactic applies an introduction rule. 
   Note that we applied the tactic to the goals in ``reverse'' order. 
   This is a trick in order to be independent from the subgoals that are 
   produced by the rule. If we had applied it in the other order 
-*}
+\<close>
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
-apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
-apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
-apply(tactic {* SUBGOAL (select_tac @{context}) 5 *})
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 1\<close>)
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 3\<close>)
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 4\<close>)
+apply(tactic \<open>SUBGOAL (select_tac @{context}) 5\<close>)
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   then we have to be careful to not apply the tactic to the two subgoals produced by 
   the first goal. To do this can result in quite messy code. In contrast, 
   the ``reverse application'' is easy to implement.
@@ -746,31 +743,31 @@
   applies theorems as shown above. The reason is that a number of theorems
   introduce schematic variables into the goal state. Consider for example the
   proof
-*}
+\<close>
 
 lemma 
   shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
-apply(tactic {* dresolve_tac @{context} [@{thm bspec}] 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>dresolve_tac @{context} [@{thm bspec}] 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]} 
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
-  where the application of theorem @{text bspec} generates two subgoals involving the
-  new schematic variable @{text "?x"}. Now, if you are not careful, tactics 
+text \<open>
+  where the application of theorem \<open>bspec\<close> generates two subgoals involving the
+  new schematic variable \<open>?x\<close>. Now, if you are not careful, tactics 
   applied to the first subgoal might instantiate this schematic variable in such a 
-  way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
+  way that the second subgoal becomes unprovable. If it is clear what the \<open>?x\<close>
   should be, then this situation can be avoided by introducing a more
-  constrained version of the @{text bspec}-theorem. One way to give such 
+  constrained version of the \<open>bspec\<close>-theorem. One way to give such 
   constraints is by pre-instantiating theorems with other theorems. 
   The function @{ML_ind RS in Drule}, for example, does this.
   
   @{ML_response_fake [display,gray]
   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
 
-  In this example it instantiates the first premise of the @{text conjI}-theorem 
-  with the theorem @{text disjI1}. If the instantiation is impossible, as in the 
+  In this example it instantiates the first premise of the \<open>conjI\<close>-theorem 
+  with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the 
   case of
 
   @{ML_response_fake_both [display,gray]
@@ -817,58 +814,58 @@
 
   \begin{isabelle}
   \isacommand{thm}~@{thm [source] cong}\\
-  @{text "> "}~@{thm cong}
+  \<open>> \<close>~@{thm cong}
   \end{isabelle}
 
   is applicable in the following proof producing the subgoals
   @{term "t x = s u"} and @{term "y = w"}. 
-*}
+\<close>
 
 lemma 
   fixes x y u w::"'a"
   shows "t x y = s u w"
 apply(rule cong)
-txt{*\begin{minipage}{\textwidth}
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   As you can see this is unfortunately \emph{not} the case if we apply @{thm [source] 
-  cong} with the method @{text rule}. The problem is
+  cong} with the method \<open>rule\<close>. The problem is
   that higher-order unification produces an instantiation that is not the
   intended one. While we can use \isacommand{back} to interactively find the
   intended instantiation, this is not an option for an automatic proof
   procedure. Fortunately, the tactic @{ML_ind cong_tac in Cong_Tac} helps 
   with applying congruence theorems and finding the intended instantiation.
   For example
-*}
+\<close>
 
 lemma 
   fixes x y u w::"'a"
   shows "t x y = s u w"
-apply(tactic {* Cong_Tac.cong_tac @{context} @{thm cong} 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>Cong_Tac.cong_tac @{context} @{thm cong} 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   However, frequently it is necessary to explicitly match a theorem against a goal
   state and in doing so construct manually an appropriate instantiation. Imagine 
   you have the theorem
-*}
+\<close>
 
 lemma rule:
   shows "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> R (f x) (g y)"
 sorry
 
-text {* 
+text \<open>
   and you want to apply it to the goal @{term "(t\<^sub>1 t\<^sub>2) \<le>
   (s\<^sub>1 s\<^sub>2)"}. Since in the theorem all variables are
-  schematic, we have a nasty higher-order unification problem and @{text rtac}
+  schematic, we have a nasty higher-order unification problem and \<open>rtac\<close>
   will not be able to apply this rule in the way we want. For the goal at hand 
-  we want to use it so that @{term R} is instantiated to the constant @{text \<le>} and
+  we want to use it so that @{term R} is instantiated to the constant \<open>\<le>\<close> and
   similarly ``obvious'' instantiations for the other variables.  To achieve this 
   we need to match the conclusion of 
   @{thm [source] rule} against the goal reading off an instantiation for
@@ -877,34 +874,34 @@
   that can be used to instantiate the theorem. The instantiation 
   can be done with the function @{ML_ind instantiate_normalize in Drule}. To automate 
   this we implement the following function.
-*}
-
-ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {context, concl, ...} =>
+\<close>
+
+ML %linenosgray\<open>fun fo_rtac thm = Subgoal.FOCUS (fn {context, concl, ...} =>
   let 
     val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm)
     val insts = Thm.first_order_match (concl_pat, concl)
   in
     resolve_tac context [(Drule.instantiate_normalize insts thm)] 1
-  end)*}
-
-text {*
+  end)\<close>
+
+text \<open>
   Note that we use @{ML FOCUS in Subgoal} because it gives us directly access
   to the conclusion of the goal state, but also because this function 
   takes care of correctly handling parameters that might be present
   in the goal state. In Line 3 we use the function @{ML_ind strip_imp_concl in Drule}
   for calculating the conclusion of a theorem (produced as @{ML_type cterm}).
   An example of @{ML fo_rtac} is as follows.
-*}
+\<close>
 
 lemma
   shows "\<And>t\<^sub>1 s\<^sub>1 (t\<^sub>2::'a) (s\<^sub>2::'a). (t\<^sub>1 t\<^sub>2) \<le> (s\<^sub>1 s\<^sub>2)"
-apply(tactic {* fo_rtac @{thm rule} @{context} 1 *})
-txt{*\begin{minipage}{\textwidth}
+apply(tactic \<open>fo_rtac @{thm rule} @{context} 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
      @{subgoals [display]}
-     \end{minipage}*}
+     \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   We obtain the intended subgoals and also the parameters are correctly
   introduced in both of them. Such manual instantiations are quite frequently
   necessary in order to appropriately constrain the application of theorems. 
@@ -916,83 +913,83 @@
   Functions for instantiating schematic variables in theorems are defined
   in @{ML_file "Pure/drule.ML"}.
   \end{readmore}
-*}
-
-section {* Tactic Combinators *}
-
-text {* 
+\<close>
+
+section \<open>Tactic Combinators\<close>
+
+text \<open>
   The purpose of tactic combinators is to build compound tactics out of
   smaller tactics. In the previous section we already used @{ML_ind THEN in Tactical}, 
   which just strings together two tactics in a sequence. For example:
-*}
+\<close>
 
 lemma 
   shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 THEN resolve_tac @{context} [@{thm conjI}] 1 *})
-txt {* \begin{minipage}{\textwidth}
+apply(tactic \<open>resolve_tac @{context} [@{thm conjI}] 1 THEN resolve_tac @{context} [@{thm conjI}] 1\<close>)
+txt \<open>\begin{minipage}{\textwidth}
        @{subgoals [display]} 
-       \end{minipage} *}
+       \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   If you want to avoid the hard-coded subgoal addressing in each component, 
   then, as seen earlier, you can use the ``primed'' version of @{ML THEN}. 
   For example:
-*}
+\<close>
 
 lemma 
   shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* (resolve_tac @{context} [@{thm conjI}] THEN' resolve_tac @{context} [@{thm conjI}]) 1 *})
-txt {* \begin{minipage}{\textwidth}
+apply(tactic \<open>(resolve_tac @{context} [@{thm conjI}] THEN' resolve_tac @{context} [@{thm conjI}]) 1\<close>)
+txt \<open>\begin{minipage}{\textwidth}
        @{subgoals [display]} 
-       \end{minipage} *}
+       \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {* 
+text \<open>
   Here you have to specify the subgoal of interest only once and it is
   consistently applied to the component.  For most tactic combinators such a
   ``primed'' version exists and in what follows we will usually prefer it over
   the ``unprimed'' one.
 
-  The tactic combinator @{ML_ind RANGE in Tactical} takes a list of @{text n}
-  tactics, say, and applies them to each of the first @{text n} subgoals. 
+  The tactic combinator @{ML_ind RANGE in Tactical} takes a list of \<open>n\<close>
+  tactics, say, and applies them to each of the first \<open>n\<close> subgoals. 
   For example below we first apply the introduction rule for conjunctions
   and then apply a tactic to each of the two subgoals. 
-*}
+\<close>
 
 lemma 
   shows "A \<Longrightarrow> True \<and> A"
-apply(tactic {* (resolve_tac @{context} [@{thm conjI}] 
-                 THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1 *})
-txt {* \begin{minipage}{\textwidth}
+apply(tactic \<open>(resolve_tac @{context} [@{thm conjI}] 
+                 THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1\<close>)
+txt \<open>\begin{minipage}{\textwidth}
        @{subgoals [display]} 
-       \end{minipage} *}
+       \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   If there is a list of tactics that should all be tried out in sequence on
   one specified subgoal, you can use the combinator @{ML_ind EVERY' in
   Tactical}. For example the function @{ML foo_tac'} from
   page~\pageref{tac:footacprime} can also be written as:
-*}
-
-ML %grayML{*fun foo_tac'' ctxt = 
+\<close>
+
+ML %grayML\<open>fun foo_tac'' ctxt = 
   EVERY' [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], 
-          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]*}
-
-text {*
+          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]\<close>
+
+text \<open>
   There is even another way of implementing this tactic: in automatic proof
   procedures (in contrast to tactics that might be called by the user) there
   are often long lists of tactics that are applied to the first
   subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"}, 
   you can also just write
-*}
-
-ML %grayML{*fun foo_tac1 ctxt = 
+\<close>
+
+ML %grayML\<open>fun foo_tac1 ctxt = 
   EVERY1 [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], 
-          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]*}
-
-text {*
+          assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]\<close>
+
+text \<open>
   and call @{ML foo_tac1}.  
 
   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind  EVERY1 in Tactical} it must be
@@ -1001,99 +998,99 @@
   then you can use the combinator @{ML_ind  ORELSE' in Tactical} for two tactics, and @{ML_ind
    FIRST' in Tactical} (or @{ML_ind  FIRST1 in Tactical}) for a list of tactics. For example, the tactic
 
-*}
-
-ML %grayML{*fun orelse_xmp_tac ctxt = 
-  resolve_tac ctxt [@{thm disjI1}] ORELSE' resolve_tac ctxt [@{thm conjI}]*}
-
-text {*
-  will first try out whether theorem @{text disjI} applies and in case of failure 
-  will try @{text conjI}. To see this consider the proof
-*}
+\<close>
+
+ML %grayML\<open>fun orelse_xmp_tac ctxt = 
+  resolve_tac ctxt [@{thm disjI1}] ORELSE' resolve_tac ctxt [@{thm conjI}]\<close>
+
+text \<open>
+  will first try out whether theorem \<open>disjI\<close> applies and in case of failure 
+  will try \<open>conjI\<close>. To see this consider the proof
+\<close>
 
 lemma 
   shows "True \<and> False" and "Foo \<or> Bar"
-apply(tactic {* orelse_xmp_tac @{context} 2 *})
-apply(tactic {* orelse_xmp_tac @{context} 1 *})
-txt {* which results in the goal state
+apply(tactic \<open>orelse_xmp_tac @{context} 2\<close>)
+apply(tactic \<open>orelse_xmp_tac @{context} 1\<close>)
+txt \<open>which results in the goal state
        \begin{isabelle}
        @{subgoals [display]} 
        \end{isabelle}
-*}
+\<close>
 (*<*)oops(*>*)
 
 
-text {*
+text \<open>
   Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} 
   as follows:
-*}
-
-ML %grayML{*fun select_tac' ctxt = 
+\<close>
+
+ML %grayML\<open>fun select_tac' ctxt = 
   FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], 
-          resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]*}text_raw{*\label{tac:selectprime}*}
-
-text {*
+          resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close>
+
+text \<open>
   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 
   we must include @{ML all_tac} at the end of the list, otherwise the tactic will
   fail if no theorem applies (we also have to wrap @{ML all_tac} using the 
   @{ML K}-combinator, because it does not take a subgoal number as argument). You can 
   test the tactic on the same goals:
-*}
+\<close>
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* select_tac' @{context} 4 *})
-apply(tactic {* select_tac' @{context} 3 *})
-apply(tactic {* select_tac' @{context} 2 *})
-apply(tactic {* select_tac' @{context} 1 *})
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>select_tac' @{context} 4\<close>)
+apply(tactic \<open>select_tac' @{context} 3\<close>)
+apply(tactic \<open>select_tac' @{context} 2\<close>)
+apply(tactic \<open>select_tac' @{context} 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]}
-      \end{minipage} *}
+      \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {* 
+text \<open>
   Since such repeated applications of a tactic to the reverse order of 
   \emph{all} subgoals is quite common, there is the tactic combinator 
   @{ML_ind  ALLGOALS in Tactical} that simplifies this. Using this combinator you can simply 
-  write: *}
+  write:\<close>
 
 lemma 
   shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* ALLGOALS (select_tac' @{context}) *})
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>ALLGOALS (select_tac' @{context})\<close>)
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]}
-      \end{minipage} *}
+      \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Remember that we chose to implement @{ML select_tac'} so that it 
   always  succeeds by fact of having @{ML all_tac} at the end of the tactic
   list. The same can be achieved with the tactic combinator @{ML_ind  TRY in Tactical}.
   For example:
-*}
-
-ML %grayML{*fun select_tac'' ctxt = 
+\<close>
+
+ML %grayML\<open>fun select_tac'' ctxt = 
  TRY o FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], 
-               resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}]]*}
-text_raw{*\label{tac:selectprimeprime}*}
-
-text {*
+               resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}]]\<close>
+text_raw\<open>\label{tac:selectprimeprime}\<close>
+
+text \<open>
   This tactic behaves in the same way as @{ML select_tac'}: it tries out
   one of the given tactics and if none applies leaves the goal state 
   unchanged. This, however, can be potentially very confusing when visible to 
   the user, for example,  in cases where the goal is the form
 
-*}
+\<close>
 
 lemma 
   shows "E \<Longrightarrow> F"
-apply(tactic {* select_tac' @{context} 1 *})
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>select_tac' @{context} 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]}
-      \end{minipage} *}
+      \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   In this case no theorem applies. But because we wrapped the tactic in a @{ML
   TRY}, it does not fail anymore. The problem is that for the user there is
   little chance to see whether progress in the proof has been made, or not. By
@@ -1106,40 +1103,40 @@
   option. In such cases, you can use the combinator @{ML_ind CHANGED in
   Tactical} to make sure the subgoal has been changed by the tactic. Because
   now
-*}
+\<close>
 
 lemma 
   shows "E \<Longrightarrow> F"
-apply(tactic {* CHANGED (select_tac' @{context} 1) *})(*<*)?(*>*)
-txt{* gives the error message:
+apply(tactic \<open>CHANGED (select_tac' @{context} 1)\<close>)(*<*)?(*>*)
+txt\<open>gives the error message:
   \begin{isabelle}
-  @{text "*** empty result sequence -- proof command failed"}\\
-  @{text "*** At command \"apply\"."}
+  \<open>*** empty result sequence -- proof command failed\<close>\\
+  \<open>*** At command "apply".\<close>
   \end{isabelle} 
-*}(*<*)oops(*>*)
-
-
-text {*
+\<close>(*<*)oops(*>*)
+
+
+text \<open>
   We can further extend the @{ML select_tac}s so that they not just apply to the topmost
   connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 
   completely. For this you can use the tactic combinator @{ML_ind REPEAT in Tactical}. As an example 
   suppose the following tactic
-*}
-
-ML %grayML{*fun repeat_xmp_tac ctxt = REPEAT (CHANGED (select_tac' ctxt 1)) *}
-
-text {* which applied to the proof *}
+\<close>
+
+ML %grayML\<open>fun repeat_xmp_tac ctxt = REPEAT (CHANGED (select_tac' ctxt 1))\<close>
+
+text \<open>which applied to the proof\<close>
 
 lemma 
   shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_xmp_tac @{context} *})
-txt{* produces
+apply(tactic \<open>repeat_xmp_tac @{context}\<close>)
+txt\<open>produces
       \begin{isabelle}
       @{subgoals [display]}
-      \end{isabelle} *}
+      \end{isabelle}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
   because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
   tactic as long as it succeeds). The function @{ML_ind REPEAT1 in Tactical}
@@ -1148,11 +1145,11 @@
 
   If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you 
   can implement it as
-*}
-
-ML %grayML{*fun repeat_xmp_tac' ctxt = REPEAT o CHANGED o select_tac' ctxt*}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun repeat_xmp_tac' ctxt = REPEAT o CHANGED o select_tac' ctxt\<close>
+
+text \<open>
   since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
 
   If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
@@ -1161,76 +1158,76 @@
   is applied repeatedly only to the first subgoal. To analyse also all
   resulting subgoals, you can use the tactic combinator @{ML_ind  REPEAT_ALL_NEW in Tactical}. 
   Supposing the tactic
-*}
-
-ML %grayML{*fun repeat_all_new_xmp_tac ctxt = REPEAT_ALL_NEW (CHANGED o select_tac' ctxt)*}
-
-text {* 
+\<close>
+
+ML %grayML\<open>fun repeat_all_new_xmp_tac ctxt = REPEAT_ALL_NEW (CHANGED o select_tac' ctxt)\<close>
+
+text \<open>
   you can see that the following goal
-*}
+\<close>
 
 lemma 
   shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_all_new_xmp_tac @{context} 1 *})
-txt{* \begin{minipage}{\textwidth}
+apply(tactic \<open>repeat_all_new_xmp_tac @{context} 1\<close>)
+txt\<open>\begin{minipage}{\textwidth}
       @{subgoals [display]}
-      \end{minipage} *}
+      \end{minipage}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   is completely analysed according to the theorems we chose to
   include in @{ML select_tac'}. 
 
   Recall that tactics produce a lazy sequence of successor goal states. These
   states can be explored using the command \isacommand{back}. For example
 
-*}
+\<close>
 
 lemma 
   shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
-txt{* applies the rule to the first assumption yielding the goal state:
+apply(tactic \<open>eresolve_tac @{context} [@{thm disjE}] 1\<close>)
+txt\<open>applies the rule to the first assumption yielding the goal state:
       \begin{isabelle}
       @{subgoals [display]}
       \end{isabelle}
 
       After typing
-  *}
+\<close>
 (*<*)
 oops
 lemma 
   shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
+apply(tactic \<open>eresolve_tac @{context} [@{thm disjE}] 1\<close>)
 (*>*)
 back
-txt{* the rule now applies to the second assumption.
+txt\<open>the rule now applies to the second assumption.
       \begin{isabelle}
       @{subgoals [display]}
-      \end{isabelle} *}
+      \end{isabelle}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Sometimes this leads to confusing behaviour of tactics and also has
   the potential to explode the search space for tactics.
   These problems can be avoided by prefixing the tactic with the tactic 
   combinator @{ML_ind  DETERM in Tactical}.
-*}
+\<close>
 
 lemma 
   shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* DETERM (eresolve_tac @{context} [@{thm disjE}] 1) *})
-txt {*\begin{minipage}{\textwidth}
+apply(tactic \<open>DETERM (eresolve_tac @{context} [@{thm disjE}] 1)\<close>)
+txt \<open>\begin{minipage}{\textwidth}
       @{subgoals [display]}
-      \end{minipage} *}
+      \end{minipage}\<close>
 (*<*)oops(*>*)
-text {*
+text \<open>
   This combinator will prune the search space to just the first successful application.
   Attempting to apply \isacommand{back} in this goal states gives the
   error message:
 
   \begin{isabelle}
-  @{text "*** back: no alternatives"}\\
-  @{text "*** At command \"back\"."}
+  \<open>*** back: no alternatives\<close>\\
+  \<open>*** At command "back".\<close>
   \end{isabelle}
 
 
@@ -1241,9 +1238,9 @@
   Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}.
   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
   \end{readmore}
-*}
-
-text {*
+\<close>
+
+text \<open>
   \begin{exercise}\label{ex:dyckhoff}
   Dyckhoff presents in \cite{Dyckhoff92} inference rules of a sequent
   calculus, called G4ip, for intuitionistic propositional logic. The
@@ -1304,11 +1301,11 @@
   equality and run your tactic on  the de Bruijn formulae discussed 
   in Exercise~\ref{ex:debruijn}.
   \end{exercise}
-*}
-
-section {* Simplifier Tactics\label{sec:simplifier} *}
-
-text {*
+\<close>
+
+section \<open>Simplifier Tactics\label{sec:simplifier}\<close>
+
+text \<open>
   A lot of convenience in reasoning with Isabelle derives from its
   powerful simplifier. We will describe it in this section. However,
   due to its complexity, we can mostly only scratch the surface. 
@@ -1323,34 +1320,34 @@
   \begin{isabelle}
   \begin{center}
   \begin{tabular}{l@ {\hspace{2cm}}l}
-   @{ML_ind simp_tac in Simplifier}            & @{text "(simp (no_asm))"} \\
-   @{ML_ind asm_simp_tac in Simplifier}        & @{text "(simp (no_asm_simp))"} \\
-   @{ML_ind full_simp_tac in Simplifier}       & @{text "(simp (no_asm_use))"} \\
-   @{ML_ind asm_lr_simp_tac in Simplifier}     & @{text "(simp (asm_lr))"} \\
-   @{ML_ind asm_full_simp_tac in Simplifier}   & @{text "(simp)"}
+   @{ML_ind simp_tac in Simplifier}            & \<open>(simp (no_asm))\<close> \\
+   @{ML_ind asm_simp_tac in Simplifier}        & \<open>(simp (no_asm_simp))\<close> \\
+   @{ML_ind full_simp_tac in Simplifier}       & \<open>(simp (no_asm_use))\<close> \\
+   @{ML_ind asm_lr_simp_tac in Simplifier}     & \<open>(simp (asm_lr))\<close> \\
+   @{ML_ind asm_full_simp_tac in Simplifier}   & \<open>(simp)\<close>
   \end{tabular}
   \end{center}
   \end{isabelle}
 
   All these tactics take a simpset and an integer as argument (the latter as usual 
   to specify  the goal to be analysed). So the proof
-*}
+\<close>
 
 lemma 
   shows "Suc (1 + 2) < 3 + 2"
 apply(simp)
 done
 
-text {*
+text \<open>
   corresponds on the ML-level to the tactic
-*}
+\<close>
 
 lemma 
   shows "Suc (1 + 2) < 3 + 2"
-apply(tactic {* asm_full_simp_tac @{context} 1 *})
+apply(tactic \<open>asm_full_simp_tac @{context} 1\<close>)
 done
 
-text {*
+text \<open>
   If the simplifier cannot make any progress, then it leaves the goal unchanged,
   i.e., does not raise any error message. That means if you use it to unfold a 
   definition for a constant and this constant is not present in the goal state, 
@@ -1380,15 +1377,15 @@
 
   \begin{isabelle}
   \begin{center}
-  \mbox{\inferrule{@{text "t\<^sub>1 \<equiv> s\<^sub>1 \<dots> t\<^sub>n \<equiv> s\<^sub>n"}}
-                  {@{text "constr t\<^sub>1\<dots>t\<^sub>n \<equiv> constr s\<^sub>1\<dots>s\<^sub>n"}}}
+  \mbox{\inferrule{\<open>t\<^sub>1 \<equiv> s\<^sub>1 \<dots> t\<^sub>n \<equiv> s\<^sub>n\<close>}
+                  {\<open>constr t\<^sub>1\<dots>t\<^sub>n \<equiv> constr s\<^sub>1\<dots>s\<^sub>n\<close>}}
   \end{center}
   \end{isabelle}
 
-  with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"}
+  with \<open>constr\<close> being a constant, like @{const "If"}, @{const "Let"}
   and so on. Every simpset contains only one congruence rule for each
   term-constructor, which however can be overwritten. The user can declare
-  lemmas to be congruence rules using the attribute @{text "[cong]"}. Note that 
+  lemmas to be congruence rules using the attribute \<open>[cong]\<close>. Note that 
   in HOL these congruence theorems are usually stated as equations, which are 
   then internally transformed into meta-equations.
 
@@ -1423,13 +1420,13 @@
   \end{tabular}
   \end{isabelle}
 
-*}
-
-text_raw {*
+\<close>
+
+text_raw \<open>
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
-\begin{isabelle}*}
-ML %grayML{*fun print_ss ctxt ss =
+\begin{isabelle}\<close>
+ML %grayML\<open>fun print_ss ctxt ss =
 let
   val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
 
@@ -1446,17 +1443,17 @@
 in
   pps |> Pretty.chunks
       |> pwriteln
-end*}
-text_raw {* 
+end\<close>
+text_raw \<open>
 \end{isabelle}
 \end{minipage}
 \caption{The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing
   all printable information stored in a simpset. We are here only interested in the 
   simplification rules, congruence rules and simprocs.\label{fig:printss}}
-\end{figure} *}
-
-
-text {* 
+\end{figure}\<close>
+
+
+text \<open>
   To see how they work, consider the function in Figure~\ref{fig:printss}, which
   prints out some parts of a simpset. If you use it to print out the components of the
   empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
@@ -1470,11 +1467,11 @@
   you can see it contains nothing. This simpset is usually not useful, except as a 
   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 
   the simplification rule @{thm [source] Diff_Int} as follows:
-*}
-
-ML %grayML{*val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
-
-text {*
+\<close>
+
+ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
+
+text \<open>
   Printing then out the components of the simpset gives:
 
   @{ML_response_fake [display,gray]
@@ -1487,11 +1484,11 @@
   \footnote{\bf FIXME: Why does it print out ??.unknown}
 
   Adding also the congruence rule @{thm [source] strong_INF_cong} 
-*}
-
-ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection}) *}
-
-text {*
+\<close>
+
+ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection})\<close>
+
+text \<open>
   gives
 
   @{ML_response_fake [display,gray]
@@ -1526,7 +1523,7 @@
   \end{isabelle}
 
   and also resolve with assumptions. For example:
-*}
+\<close>
 
 lemma 
  shows "True" 
@@ -1534,10 +1531,10 @@
   and  "t \<equiv> t" 
   and  "False \<Longrightarrow> Foo" 
   and  "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
-apply(tactic {* ALLGOALS (simp_tac (put_simpset HOL_basic_ss @{context})) *})
+apply(tactic \<open>ALLGOALS (simp_tac (put_simpset HOL_basic_ss @{context}))\<close>)
 done
 
-text {*
+text \<open>
   This behaviour is not because of simplification rules, but how the subgoaler, solver 
   and looper are set up in @{ML HOL_basic_ss}.
 
@@ -1568,33 +1565,33 @@
   simplifier implements the tactic @{ML_ind rewrite_goal_tac in Raw_Simplifier}.\footnote{\bf FIXME: 
   see LocalDefs infrastructure.} Suppose for example the
   definition
-*}
+\<close>
 
 definition "MyTrue \<equiv> True"
 
-text {*
+text \<open>
   then we can use this tactic to unfold the definition of this constant.
-*}
+\<close>
 
 lemma 
   shows "MyTrue \<Longrightarrow> True"
-apply(tactic {* rewrite_goal_tac @{context} @{thms MyTrue_def} 1 *})
-txt{* producing the goal state
+apply(tactic \<open>rewrite_goal_tac @{context} @{thms MyTrue_def} 1\<close>)
+txt\<open>producing the goal state
       \begin{isabelle}
       @{subgoals [display]}
-      \end{isabelle} *}
+      \end{isabelle}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   If you want to unfold definitions in \emph{all} subgoals, not just one, 
   then use the the tactic @{ML_ind rewrite_goals_tac in Raw_Simplifier}.
-*}
-
-
-text_raw {*
+\<close>
+
+
+text_raw \<open>
 \begin{figure}[p]
 \begin{boxedminipage}{\textwidth}
-\begin{isabelle} *}
+\begin{isabelle}\<close>
 type_synonym  prm = "(nat \<times> nat) list"
 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
 
@@ -1643,7 +1640,7 @@
 fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
 shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>c) = (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>(pi\<^sub>1\<bullet>c)" 
 by (induct pi\<^sub>2) (auto)
-text_raw {*
+text_raw \<open>
 \end{isabelle}
 \end{boxedminipage}
 \caption{A simple theory about permutations over @{typ nat}s. The point is that the
@@ -1651,10 +1648,10 @@
   it would cause the simplifier to loop. It can still be used as a simplification 
   rule if the permutation in the right-hand side is sufficiently protected.
   \label{fig:perms}}
-\end{figure} *}
-
-
-text {*
+\end{figure}\<close>
+
+
+text \<open>
   The simplifier is often used in order to bring terms into a normal form.
   Unfortunately, often the situation arises that the corresponding
   simplification rules will cause the simplifier to run into an infinite
@@ -1667,7 +1664,7 @@
   the right-hand side of this lemma is again an instance of the left-hand side 
   and so causes an infinite loop. There seems to be no easy way to reformulate 
   this rule and so one ends up with clunky proofs like:
-*}
+\<close>
 
 lemma 
 fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
@@ -1678,19 +1675,19 @@
 apply(simp)
 done 
 
-text {*
+text \<open>
   It is however possible to create a single simplifier tactic that solves
   such proofs. The trick is to introduce an auxiliary constant for permutations 
   and split the simplification into two phases (below actually three). Let 
   assume the auxiliary constant is
-*}
+\<close>
 
 definition
   perm_aux :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet>aux _" [80,80] 80)
 where
   "pi \<bullet>aux c \<equiv> pi \<bullet> c"
 
-text {* Now the two lemmas *}
+text \<open>Now the two lemmas\<close>
 
 lemma perm_aux_expand:
   fixes c::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
@@ -1702,7 +1699,7 @@
   shows "pi\<^sub>1\<bullet>(pi\<^sub>2\<bullet>aux c) = (pi\<^sub>1\<bullet>pi\<^sub>2) \<bullet>aux (pi\<^sub>1\<bullet>c)" 
 unfolding perm_aux_def by (rule perm_compose)
 
-text {* 
+text \<open>
   are simple consequence of the definition and @{thm [source] perm_compose}. 
   More importantly, the lemma @{thm [source] perm_compose_aux} can be safely 
   added to the simplifier, because now the right-hand side is not anymore an instance 
@@ -1715,9 +1712,9 @@
   other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
   finally ``unfreeze'' all instances of permutation compositions by unfolding 
   the definition of the auxiliary constant. 
-*}
-
-ML %linenosgray{*fun perm_simp_tac ctxt =
+\<close>
+
+ML %linenosgray\<open>fun perm_simp_tac ctxt =
 let
   val thms1 = [@{thm perm_aux_expand}]
   val thms2 = [@{thm perm_append}, @{thm perm_bij}, @{thm perm_rev}, 
@@ -1729,22 +1726,22 @@
   simp_tac (ss addsimps thms1)
   THEN' simp_tac (ss addsimps thms2)
   THEN' simp_tac (ss addsimps thms3)
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   For all three phases we have to build simpsets adding specific lemmas. As is sufficient
   for our purposes here, we can add these lemmas to @{ML HOL_basic_ss} in order to obtain
   the desired results. Now we can solve the following lemma
-*}
+\<close>
 
 lemma 
   fixes c d::"nat" and pi\<^sub>1 pi\<^sub>2::"prm"
   shows "pi\<^sub>1\<bullet>(c, pi\<^sub>2\<bullet>((rev pi\<^sub>1)\<bullet>d)) = (pi\<^sub>1\<bullet>c, (pi\<^sub>1\<bullet>pi\<^sub>2)\<bullet>d)"
-apply(tactic {* perm_simp_tac @{context} 1 *})
+apply(tactic \<open>perm_simp_tac @{context} 1\<close>)
 done
 
 
-text {*
+text \<open>
   in one step. This tactic can deal with most instances of normalising permutations.
   In order to solve all cases we have to deal with corner-cases such as the
   lemma being an exact instance of the permutation composition lemma. This can
@@ -1760,11 +1757,11 @@
 
   (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
 
-*}
-
-section {* Simprocs *}
-
-text {*
+\<close>
+
+section \<open>Simprocs\<close>
+
+text \<open>
   In Isabelle you can also implement custom simplification procedures, called
   \emph{simprocs}. Simprocs can be triggered by the simplifier on a specified
   term-pattern and rewrite a term according to a theorem. They are useful in
@@ -1774,17 +1771,17 @@
   To see how simprocs work, let us first write a simproc that just prints out
   the pattern which triggers it and otherwise does nothing. For this
   you can use the function:
-*}
-
-ML %linenosgray{*fun fail_simproc ctxt redex = 
+\<close>
+
+ML %linenosgray\<open>fun fail_simproc ctxt redex = 
 let
   val _ = pwriteln (Pretty.block 
     [Pretty.str "The redex: ", pretty_cterm ctxt redex])
 in
   NONE
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   This function takes a simpset and a redex (a @{ML_type cterm}) as
   arguments. In Lines 3 and~4, we first extract the context from the given
   simpset and then print out a message containing the redex.  The function
@@ -1792,28 +1789,28 @@
   moment we are \emph{not} interested in actually rewriting anything. We want
   that the simproc is triggered by the pattern @{term "Suc n"}. This can be
   done by adding the simproc to the current simpset as follows
-*}
-
-simproc_setup %gray fail ("Suc n") = {* K fail_simproc *}
-
-text {*
+\<close>
+
+simproc_setup %gray fail ("Suc n") = \<open>K fail_simproc\<close>
+
+text \<open>
   where the second argument specifies the pattern and the right-hand side
   contains the code of the simproc (we have to use @{ML K} since we are ignoring
   an argument about morphisms. 
   After this, the simplifier is aware of the simproc and you can test whether 
   it fires on the lemma:
-*}
+\<close>
 
 lemma 
   shows "Suc 0 = 1"
 apply(simp)
-txt{*
+txt\<open>
   \begin{minipage}{\textwidth}
-  \small@{text "> The redex: Suc 0"}\\
-  @{text "> The redex: Suc 0"}\\
-  \end{minipage}*}(*<*)oops(*>*)
-
-text {* 
+  \small\<open>> The redex: Suc 0\<close>\\
+  \<open>> The redex: Suc 0\<close>\\
+  \end{minipage}\<close>(*<*)oops(*>*)
+
+text \<open>
   This will print out the message twice: once for the left-hand side and
   once for the right-hand side. The reason is that during simplification the
   simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
@@ -1822,23 +1819,23 @@
   We can add or delete the simproc from the current simpset by the usual 
   \isacommand{declare}-statement. For example the simproc will be deleted
   with the declaration
-*}
+\<close>
 
 declare [[simproc del: fail]]
 
-text {*
+text \<open>
   If you want to see what happens with just \emph{this} simproc, without any 
-  interference from other rewrite rules, you can call @{text fail} 
+  interference from other rewrite rules, you can call \<open>fail\<close> 
   as follows:
-*}
+\<close>
 
 lemma 
   shows "Suc 0 = 1"
-apply(tactic {* simp_tac (put_simpset 
-  HOL_basic_ss @{context} addsimprocs [@{simproc fail}]) 1*})
+apply(tactic \<open>simp_tac (put_simpset 
+  HOL_basic_ss @{context} addsimprocs [@{simproc fail}]) 1\<close>)
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   Now the message shows up only once since the term @{term "1::nat"} is 
   left unchanged. 
 
@@ -1847,28 +1844,28 @@
   want this, then you have to use a slightly different method for setting 
   up the simproc. First the function @{ML fail_simproc} needs to be modified
   to
-*}
-
-ML %grayML{*fun fail_simproc' _ ctxt redex = 
+\<close>
+
+ML %grayML\<open>fun fail_simproc' _ ctxt redex = 
 let
   val _ = pwriteln (Pretty.block 
     [Pretty.str "The redex:", pretty_cterm ctxt redex])
 in
   NONE
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
   (therefore we printing it out using the function @{ML pretty_term in Pretty}).
   We can turn this function into a proper simproc using the function 
   @{ML Simplifier.make_simproc}:
-*}
-
-ML %grayML{*val fail' = 
+\<close>
+
+ML %grayML\<open>val fail' = 
   Simplifier.make_simproc @{context} "fail_simproc'"
-    {lhss = [@{term "Suc n"}], proc = fail_simproc'}*}
-
-text {*
+    {lhss = [@{term "Suc n"}], proc = fail_simproc'}\<close>
+
+text \<open>
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
   The function also takes a list of patterns that can trigger the simproc.
   Now the simproc is set up and can be explicitly added using
@@ -1877,14 +1874,14 @@
 
   Simprocs are applied from inside to outside and from left to right. You can
   see this in the proof
-*}
+\<close>
 
 lemma 
   shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail']) 1*})
+apply(tactic \<open>simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail']) 1\<close>)
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   The simproc @{ML fail'} prints out the sequence 
 
 @{text [display]
@@ -1894,52 +1891,52 @@
 
   To see how a simproc applies a theorem,  let us implement a simproc that
   rewrites terms according to the equation:
-*}
+\<close>
 
 lemma plus_one: 
   shows "Suc n \<equiv> n + 1" by simp
 
-text {*
+text \<open>
   Simprocs expect that the given equation is a meta-equation, however the
   equation can contain preconditions (the simproc then will only fire if the
   preconditions can be solved). To see that one has relatively precise control over
   the rewriting with simprocs, let us further assume we want that the simproc
   only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write 
-*}
-
-
-ML %grayML{*fun plus_one_simproc _ ctxt redex =
+\<close>
+
+
+ML %grayML\<open>fun plus_one_simproc _ ctxt redex =
   case Thm.term_of redex of
     @{term "Suc 0"} => NONE
-  | _ => SOME @{thm plus_one}*}
-
-text {*
+  | _ => SOME @{thm plus_one}\<close>
+
+text \<open>
   and set up the simproc as follows.
-*}
-
-ML %grayML{*val plus_one =
+\<close>
+
+ML %grayML\<open>val plus_one =
   Simplifier.make_simproc @{context} "sproc +1"
-    {lhss = [@{term "Suc n"}], proc = plus_one_simproc}*}
-
-text {*
+    {lhss = [@{term "Suc n"}], proc = plus_one_simproc}\<close>
+
+text \<open>
   Now the simproc is set up so that it is triggered by terms
   of the form @{term "Suc n"}, but inside the simproc we only produce
   a theorem if the term is not @{term "Suc 0"}. The result you can see
   in the following proof
-*}
+\<close>
 
 lemma 
   shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one]) 1*})
-txt{*
+apply(tactic \<open>simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one]) 1\<close>)
+txt\<open>
   where the simproc produces the goal state
   \begin{isabelle}
   @{subgoals[display]}
   \end{isabelle}
-*}  
+\<close>  
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   As usual with rewriting you have to worry about looping: you already have
   a loop with @{ML plus_one}, if you apply it with the default simpset (because
   the default simpset contains a rule which just does the opposite of @{ML plus_one},
@@ -1947,50 +1944,50 @@
   in choosing the right simpset to which you add a simproc. 
 
   Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
-  with the number @{text n} increased by one. First we implement a function that
+  with the number \<open>n\<close> increased by one. First we implement a function that
   takes a term and produces the corresponding integer value.
-*}
-
-ML %grayML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
-  | dest_suc_trm t = snd (HOLogic.dest_number t)*}
-
-text {* 
+\<close>
+
+ML %grayML\<open>fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
+  | dest_suc_trm t = snd (HOLogic.dest_number t)\<close>
+
+text \<open>
   It uses the library function @{ML_ind  dest_number in HOLogic} that transforms
   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
   on, into integer values. This function raises the exception @{ML TERM}, if
   the term is not a number. The next function expects a pair consisting of a term
-  @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. 
-*}
-
-ML %linenosgray{*fun get_thm ctxt (t, n) =
+  \<open>t\<close> (containing @{term Suc}s) and the corresponding integer value \<open>n\<close>. 
+\<close>
+
+ML %linenosgray\<open>fun get_thm ctxt (t, n) =
 let
   val num = HOLogic.mk_number @{typ "nat"} n
   val goal = Logic.mk_equals (t, num)
 in
   Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   From the integer value it generates the corresponding number term, called 
-  @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 
+  \<open>num\<close> (Line 3), and then generates the meta-equation \<open>t \<equiv> num\<close> 
   (Line 4), which it proves by the arithmetic tactic in Line 6. 
 
   For our purpose at the moment, proving the meta-equation using @{ML
   arith_tac in Arith_Data} is fine, but there is also an alternative employing
   the simplifier with a special simpset. For the kind of lemmas we
-  want to prove here, the simpset @{text "num_ss"} should suffice.
-*}
-
-ML %grayML{*fun get_thm_alt ctxt (t, n) =
+  want to prove here, the simpset \<open>num_ss\<close> should suffice.
+\<close>
+
+ML %grayML\<open>fun get_thm_alt ctxt (t, n) =
 let
   val num = HOLogic.mk_number @{typ "nat"} n
   val goal = Logic.mk_equals (t, num)
   val num_ss = put_simpset HOL_ss ctxt addsimps @{thms semiring_norm}
 in
   Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   The advantage of @{ML get_thm_alt} is that it leaves very little room for 
   something to go wrong; in contrast it is much more difficult to predict 
   what happens with @{ML arith_tac in Arith_Data}, especially in more complicated 
@@ -2003,39 +2000,39 @@
 
   Anyway, either version can be used in the function that produces the actual 
   theorem for the simproc.
-*}
-
-ML %grayML{*fun nat_number_simproc _ ctxt ct =
+\<close>
+
+ML %grayML\<open>fun nat_number_simproc _ ctxt ct =
   SOME (get_thm_alt ctxt (Thm.term_of ct, dest_suc_trm (Thm.term_of ct)))
-  handle TERM _ => NONE *}
-
-text {*
+  handle TERM _ => NONE\<close>
+
+text \<open>
   This function uses the fact that @{ML dest_suc_trm} might raise an exception 
   @{ML TERM}. In this case there is nothing that can be rewritten and therefore no
   theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc 
   on an example, you can set it up as follows:
-*}
-
-ML %grayML{*val nat_number =
+\<close>
+
+ML %grayML\<open>val nat_number =
   Simplifier.make_simproc @{context} "nat_number"
-    {lhss = [@{term "Suc n"}], proc = nat_number_simproc}*}
-
-
-text {* 
+    {lhss = [@{term "Suc n"}], proc = nat_number_simproc}\<close>
+
+
+text \<open>
   Now in the lemma
-  *}
+\<close>
 
 lemma 
   shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number]) 1*})
-txt {* 
+apply(tactic \<open>simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number]) 1\<close>)
+txt \<open>
   you obtain the more legible goal state
   \begin{isabelle}
   @{subgoals [display]}
-  \end{isabelle}*}
+  \end{isabelle}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot 
   rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
   into a number. To solve this problem have a look at the next exercise. 
@@ -2048,21 +2045,21 @@
 
   (FIXME: We did not do anything with morphisms. Anything interesting
   one can say about them?)
-*}
-
-section {* Conversions\label{sec:conversion} *}
-
-text {*
+\<close>
+
+section \<open>Conversions\label{sec:conversion}\<close>
+
+text \<open>
   Conversions are a thin layer on top of Isabelle's inference kernel, and can
   be viewed as a controllable, bare-bone version of Isabelle's simplifier.
   The purpose of conversions is to manipulate @{ML_type cterm}s. However,
   we will also show in this section how conversions can be applied to theorems
   and to goal states. The type of conversions is
-*}
-
-ML %grayML{*type conv = cterm -> thm*}
-
-text {*
+\<close>
+
+ML %grayML\<open>type conv = cterm -> thm\<close>
+
+text \<open>
   whereby the produced theorem is always a meta-equality. A simple conversion
   is the function @{ML_ind  all_conv in Conv}, which maps a @{ML_type cterm} to an
   instance of the (meta)reflexivity theorem. For example:
@@ -2140,12 +2137,12 @@
   @{ML_ind  rewr_conv in Conv}, which expects a meta-equation as an 
   argument. Suppose the following meta-equation.
   
-*}
+\<close>
 
 lemma true_conj1: 
   shows "True \<and> P \<equiv> P" by simp
 
-text {* 
+text \<open>
   It can be used for example to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"} 
   to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
 
@@ -2232,11 +2229,11 @@
 end"
 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
 
-  The reason for this behaviour is that @{text "(op \<or>)"} expects two
-  arguments.  Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
-  conversion is then applied to @{text "t2"}, which in the example above
+  The reason for this behaviour is that \<open>(op \<or>)\<close> expects two
+  arguments.  Therefore the term must be of the form \<open>(Const \<dots> $ t1) $ t2\<close>. The
+  conversion is then applied to \<open>t2\<close>, which in the example above
   stands for @{term "True \<and> Q"}. The function @{ML fun_conv in Conv} would apply
-  the conversion to the term @{text "(Const \<dots> $ t1)"}.
+  the conversion to the term \<open>(Const \<dots> $ t1)\<close>.
 
   The function @{ML_ind  abs_conv in Conv} applies a conversion under an 
   abstraction. For example:
@@ -2251,7 +2248,7 @@
   "\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo"}
   
   Note that this conversion needs a context as an argument. We also give the
-  conversion as @{text "(K conv)"}, which is a function that ignores its
+  conversion as \<open>(K conv)\<close>, which is a function that ignores its
   argument (the argument being a sufficiently freshened version of the
   variable that is abstracted and a context). The conversion that goes under
   an application is @{ML_ind  combination_conv in Conv}. It expects two
@@ -2263,19 +2260,19 @@
   We can now apply all these functions in a conversion that recursively
   descends a term and applies a ``@{thm [source] true_conj1}''-conversion 
   in all possible positions.
-*}
-
-ML %linenosgray{*fun true_conj1_conv ctxt ctrm =
+\<close>
+
+ML %linenosgray\<open>fun true_conj1_conv ctxt ctrm =
   case (Thm.term_of ctrm) of
     @{term "(\<and>)"} $ @{term True} $ _ => 
       (Conv.arg_conv (true_conj1_conv ctxt) then_conv
          Conv.rewr_conv @{thm true_conj1}) ctrm
   | _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
   | Abs _ => Conv.abs_conv (fn (_, ctxt) => true_conj1_conv ctxt) ctxt ctrm
-  | _ => Conv.all_conv ctrm*}
-
-text {*
-  This function ``fires'' if the term is of the form @{text "(True \<and> \<dots>)"}. 
+  | _ => Conv.all_conv ctrm\<close>
+
+text \<open>
+  This function ``fires'' if the term is of the form \<open>(True \<and> \<dots>)\<close>. 
   It descends under applications (Line 6) and abstractions 
   (Line 7); otherwise it leaves the term unchanged (Line 8). In Line 2
   we need to transform the @{ML_type cterm} into a @{ML_type term} in order
@@ -2290,28 +2287,28 @@
   conv ctrm
 end"
   "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
-*}
-
-text {*
+\<close>
+
+text \<open>
   Conversions that traverse terms, like @{ML true_conj1_conv} above, can be
   implemented more succinctly with the combinators @{ML_ind bottom_conv in
   Conv} and @{ML_ind top_conv in Conv}. For example:
-*}
-
-ML %grayML{*fun true_conj1_conv ctxt =
+\<close>
+
+ML %grayML\<open>fun true_conj1_conv ctxt =
 let
   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
 in
   Conv.bottom_conv (K conv) ctxt
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   If we regard terms as trees with variables and constants on the top, then 
   @{ML bottom_conv in Conv} traverses first the the term and
   on the ``way down'' applies the conversion, whereas @{ML top_conv in
   Conv} applies the conversion on the ``way up''. To see the difference, 
   assume the following two meta-equations
-*}
+\<close>
 
 lemma conj_assoc:
   fixes A B C::bool
@@ -2319,8 +2316,8 @@
   and   "(A \<and> B) \<and> C \<equiv> A \<and> (B \<and> C)"
 by simp_all
 
-text {*
-  and the @{ML_type cterm} @{text "(a \<and> (b \<and> c)) \<and> d"}. Here you should
+text \<open>
+  and the @{ML_type cterm} \<open>(a \<and> (b \<and> c)) \<and> d\<close>. Here you should
   pause for a moment to be convinced that rewriting top-down and bottom-up 
   according to the two meta-equations produces two results. Below these
   two results are calculated. 
@@ -2340,19 +2337,19 @@
 
   To see how much control you have over rewriting with conversions, let us 
   make the task a bit more complicated by rewriting according to the rule
-  @{text true_conj1}, but only in the first arguments of @{term If}s. Then 
+  \<open>true_conj1\<close>, but only in the first arguments of @{term If}s. Then 
   the conversion should be as follows.
-*}
-
-ML %grayML{*fun if_true1_simple_conv ctxt ctrm =
+\<close>
+
+ML %grayML\<open>fun if_true1_simple_conv ctxt ctrm =
   case Thm.term_of ctrm of
     Const (@{const_name If}, _) $ _ =>
       Conv.arg_conv (true_conj1_conv ctxt) ctrm
   | _ => Conv.no_conv ctrm 
 
-val if_true1_conv = Conv.top_sweep_conv if_true1_simple_conv*}
-
-text {*
+val if_true1_conv = Conv.top_sweep_conv if_true1_simple_conv\<close>
+
+text \<open>
   In the first function we only treat the top-most redex and also only the
   success case. As default we return @{ML no_conv in Conv}.  To apply this
   ``simple'' conversion inside a term, we use in the last line the combinator @{ML_ind
@@ -2370,18 +2367,18 @@
 end"
 "if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False 
 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
-*}
-
-text {*
+\<close>
+
+text \<open>
   So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
   also work on theorems using the function @{ML_ind  fconv_rule in Conv}. As an example, 
   consider again the conversion @{ML true_conj1_conv} and the lemma:
-*}
+\<close>
 
 lemma foo_test: 
   shows "P \<or> (True \<and> \<not>P)" by simp
 
-text {*
+text \<open>
   Using the conversion you can transform this theorem into a 
   new theorem as follows
 
@@ -2402,7 +2399,7 @@
 
   \begin{itemize}
   \item @{ML_ind params_conv in Conv} for converting under parameters
-  (i.e.~where a goal state is of the form @{text "\<And>x. P x \<Longrightarrow> Q x"})
+  (i.e.~where a goal state is of the form \<open>\<And>x. P x \<Longrightarrow> Q x\<close>)
 
   \item @{ML_ind prems_conv in Conv} for applying a conversion to 
   premises of a goal state, and
@@ -2414,35 +2411,35 @@
   Assume we want to apply @{ML true_conj1_conv} only in the conclusion
   of the goal, and @{ML if_true1_conv} should only apply to the premises.
   Here is a tactic doing exactly that:
-*}
-
-ML %grayML{*fun true1_tac ctxt =
+\<close>
+
+ML %grayML\<open>fun true1_tac ctxt =
   CONVERSION 
     (Conv.params_conv ~1 (fn ctxt =>
        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
-          Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}
-
-text {* 
+          Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)\<close>
+
+text \<open>
   We call the conversions with the argument @{ML "~1"}. By this we 
   analyse all parameters, all premises and the conclusion of a goal
   state. If we call @{ML concl_conv in Conv} with 
-  a non-negative number, say @{text n}, then this conversions will 
-  skip the first @{text n} premises and applies the conversion to the 
+  a non-negative number, say \<open>n\<close>, then this conversions will 
+  skip the first \<open>n\<close> premises and applies the conversion to the 
   ``rest'' (similar for parameters and conclusions). To test the 
   tactic, consider the proof
-*}
+\<close>
 
 lemma
   "if True \<and> P then P else True \<and> False \<Longrightarrow>
   (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
-apply(tactic {* true1_tac @{context} 1 *})
-txt {* where the tactic yields the goal state
+apply(tactic \<open>true1_tac @{context} 1\<close>)
+txt \<open>where the tactic yields the goal state
   \begin{isabelle}
   @{subgoals [display]}
-  \end{isabelle}*}
+  \end{isabelle}\<close>
 (*<*)oops(*>*)
 
-text {*
+text \<open>
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
   the conclusion according to @{ML true_conj1_conv}. If we only have one
   conversion that should be uniformly applied to the whole goal state, we
@@ -2451,7 +2448,7 @@
   Conversions are also be helpful for constructing meta-equality theorems.
   Such theorems are often definitions. As an example consider the following
   two ways of defining the identity function in Isabelle. 
-*}
+\<close>
 
 definition id1::"'a \<Rightarrow> 'a" 
 where "id1 x \<equiv> x"
@@ -2459,7 +2456,7 @@
 definition id2::"'a \<Rightarrow> 'a"
 where "id2 \<equiv> \<lambda>x. x"
 
-text {*
+text \<open>
   Although both definitions define the same function, the theorems @{thm
   [source] id1_def} and @{thm [source] id2_def} are different meta-equations. However it is
   easy to transform one into the other. The function @{ML_ind abs_def
@@ -2478,9 +2475,9 @@
   @{ML_type cterm} to a conversion we obtain a meta-equality theorem (recall
   that the type of conversions is an abbreviation for 
   @{ML_type "cterm -> thm"}). The code of the transformation is below.
-*}
-
-ML %linenosgray{*fun unabs_def ctxt def =
+\<close>
+
+ML %linenosgray\<open>fun unabs_def ctxt def =
 let
   val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of def)
   val xs = strip_abs_vars (Thm.term_of rhs)
@@ -2494,16 +2491,16 @@
 in
   get_conv xs new_lhs |>  
   singleton (Proof_Context.export ctxt' ctxt)
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   In Line 3 we destruct the meta-equality into the @{ML_type cterm}s
   corresponding to the left-hand and right-hand side of the meta-equality. The
   assumption in @{ML unabs_def} is that the right-hand side is an
   abstraction. We compute the possibly empty list of abstracted variables in
   Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to
   first transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we
-  import these variables into the context @{text "ctxt'"}, in order to
+  import these variables into the context \<open>ctxt'\<close>, in order to
   export them again in Line 15.  In Line 8 we certify the list of variables,
   which in turn we apply to the @{ML_text lhs} of the definition using the
   function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the
@@ -2513,15 +2510,15 @@
   conversion with @{ML_ind fun_conv in Conv}. Now in Line 14 we only have to
   apply the new left-hand side to the generated conversion and obtain the the
   theorem we want to construct. As mentioned above, in Line 15 we only have to
-  export the context @{text "ctxt'"} back to @{text "ctxt"} in order to 
+  export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to 
   produce meta-variables for the theorem.  An example is as follows.
 
   @{ML_response_fake [display, gray]
   "unabs_def @{context} @{thm id2_def}"
   "id2 ?x1 \<equiv> ?x1"}
-*}
-
-text {*
+\<close>
+
+text \<open>
   To sum up this section, conversions are more general than the simplifier
   or simprocs, but you have to do more work yourself. Also conversions are
   often much less efficient than the simplifier. The advantage of conversions, 
@@ -2547,19 +2544,19 @@
   @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/raw_simplifier.ML"}.
   \end{readmore}
 
-*}
-
-text {*
+\<close>
+
+text \<open>
   (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term}
   are of any use/efficient)
-*}
-
-
-section {* Declarations (TBD) *}
-
-section {* Structured Proofs\label{sec:structured} (TBD) *}
-
-text {* TBD *}
+\<close>
+
+
+section \<open>Declarations (TBD)\<close>
+
+section \<open>Structured Proofs\label{sec:structured} (TBD)\<close>
+
+text \<open>TBD\<close>
 
 lemma True
 proof
@@ -2581,7 +2578,7 @@
   }
 oops
 
-ML {* 
+ML \<open>
   val ctxt0 = @{context};
   val ctxt = ctxt0;
   val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;
@@ -2591,15 +2588,15 @@
   val this = r OF this;
   val this = Assumption.export false ctxt ctxt0 this 
   val this = Variable.export ctxt ctxt0 [this] 
-*}
-
-section {* Summary *}
-
-text {*
+\<close>
+
+section \<open>Summary\<close>
+
+text \<open>
 
   \begin{conventions}
   \begin{itemize}
-  \item Reference theorems with the antiquotation @{text "@{thm \<dots>}"}.
+  \item Reference theorems with the antiquotation \<open>@{thm \<dots>}\<close>.
   \item If a tactic is supposed to fail, return the empty sequence.
   \item If you apply a tactic to a sequence of subgoals, apply it 
   in reverse order (i.e.~start with the last subgoal). 
@@ -2607,6 +2604,6 @@
   \end{itemize}
   \end{conventions}
 
-*}
+\<close>
 
 end




