src/Doc/Eisbach/Manual.thy

--- a/src/Doc/Eisbach/Manual.thy	Sun Oct 18 21:30:01 2015 +0200
+++ b/src/Doc/Eisbach/Manual.thy	Sun Oct 18 22:57:09 2015 +0200
@@ -58,7 +58,7 @@
 text \<open>
   In this example, the facts @{text impI} and @{text conjE} are static. They
   are evaluated once when the method is defined and cannot be changed later.
-  This makes the method stable in the sense of \emph{static scoping}: naming
+  This makes the method stable in the sense of \<^emph>\<open>static scoping\<close>: naming
   another fact @{text impI} in a later context won't affect the behaviour of
   @{text "prop_solver\<^sub>1"}.
 \<close>
@@ -103,7 +103,7 @@
   A @{text "named theorem"} is a fact whose contents are produced dynamically
   within the current proof context. The Isar command @{command_ref
   "named_theorems"} provides simple access to this concept: it declares a
-  dynamic fact with corresponding \emph{attribute} for managing
+  dynamic fact with corresponding \<^emph>\<open>attribute\<close> for managing
   this particular data slot in the context.
 \<close>
 
@@ -171,10 +171,10 @@
 section \<open>Higher-order methods\<close>
 
 text \<open>
-  The \emph{structured concatenation} combinator ``@{text "method\<^sub>1 ;
+  The \<^emph>\<open>structured concatenation\<close> combinator ``@{text "method\<^sub>1 ;
   method\<^sub>2"}'' was introduced in Isabelle2015, motivated by development of
   Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text
-  method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from
+  method\<^sub>2} is invoked on on \<^emph>\<open>all\<close> subgoals that have newly emerged from
   @{text method\<^sub>1}. This is useful to handle cases where the number of
   subgoals produced by a method is determined dynamically at run-time.
 \<close>
@@ -192,7 +192,7 @@
   method combinators with prefix syntax. For example, to more usefully exploit
   Isabelle's backtracking, the explicit requirement that a method solve all
   produced subgoals is frequently useful. This can easily be written as a
-  \emph{higher-order method} using ``@{text ";"}''. The @{keyword "methods"}
+  \<^emph>\<open>higher-order method\<close> using ``@{text ";"}''. The @{keyword "methods"}
   keyword denotes method parameters that are other proof methods to be invoked
   by the method being defined.
 \<close>
@@ -300,9 +300,9 @@
 
   Matching allows methods to introspect the goal state, and to implement more
   explicit control flow. In the basic case, a term or fact @{text ts} is given
-  to match against as a \emph{match target}, along with a collection of
+  to match against as a \<^emph>\<open>match target\<close>, along with a collection of
   pattern-method pairs @{text "(p, m)"}: roughly speaking, when the pattern
-  @{text p} matches any member of @{text ts}, the \emph{inner} method @{text
+  @{text p} matches any member of @{text ts}, the \<^emph>\<open>inner\<close> method @{text
   m} will be executed.
 \<close>
 
@@ -327,8 +327,8 @@
 text\<open>
   In the previous example we were able to match against an assumption out of
   the Isar proof state. In general, however, proof subgoals can be
-  \emph{unstructured}, with goal parameters and premises arising from rule
-  application. To address this, @{method match} uses \emph{subgoal focusing}
+  \<^emph>\<open>unstructured\<close>, with goal parameters and premises arising from rule
+  application. To address this, @{method match} uses \<^emph>\<open>subgoal focusing\<close>
   to produce structured goals out of
   unstructured ones. In place of fact or term, we may give the
   keyword @{keyword_def "premises"} as the match target. This causes a subgoal
@@ -467,11 +467,11 @@
 subsubsection \<open>Inner focusing\<close>
 
 text \<open>
-  Premises are \emph{accumulated} for the purposes of subgoal focusing.
+  Premises are \<^emph>\<open>accumulated\<close> for the purposes of subgoal focusing.
   In contrast to using standard methods like @{method frule} within
   focused match, another @{method match} will have access to all the premises
   of the outer focus.
-  \<close>
+\<close>
 
     lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
       by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H,
@@ -551,8 +551,8 @@
 text \<open>
   The @{attribute of} attribute behaves similarly. It is worth noting,
   however, that the positional instantiation of @{attribute of} occurs against
-  the position of the variables as they are declared \emph{in the match
-  pattern}.
+  the position of the variables as they are declared \<^emph>\<open>in the match
+  pattern\<close>.
 \<close>
 
     lemma
@@ -569,7 +569,7 @@
   declared the @{typ 'a} slot first and the @{typ 'b} slot second.
 
   To get the dynamic behaviour of @{attribute of} we can choose to invoke it
-  \emph{unchecked}. This avoids trying to do any type inference for the
+  \<^emph>\<open>unchecked\<close>. This avoids trying to do any type inference for the
   provided parameters, instead storing them as their most general type and
   doing type matching at run-time. This, like @{attribute OF}, will throw
   errors if the expected slots don't exist or there is a type mismatch.
@@ -605,7 +605,7 @@
 text \<open>
   In all previous examples, @{method match} was only ever searching for a
   single rule or premise. Each local fact would therefore always have a length
-  of exactly one. We may, however, wish to find \emph{all} matching results.
+  of exactly one. We may, however, wish to find \<^emph>\<open>all\<close> matching results.
   To achieve this, we can simply mark a given pattern with the @{text
   "(multi)"} argument.
 \<close>
@@ -806,7 +806,7 @@
 text \<open>
   The @{method match} method is not aware of the logical content of match
   targets. Each pattern is simply matched against the shallow structure of a
-  fact or term. Most facts are in \emph{normal form}, which curries premises
+  fact or term. Most facts are in \<^emph>\<open>normal form\<close>, which curries premises
   via meta-implication @{text "_ \<Longrightarrow> _"}.
 \<close>
 
@@ -835,11 +835,11 @@
   to @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a
   concrete @{term "C"} in the conclusion, will fail to match this fact.
 
-  To express our desired match, we may \emph{uncurry} our rules before
+  To express our desired match, we may \<^emph>\<open>uncurry\<close> our rules before
   matching against them. This forms a meta-conjunction of all premises in a
   fact, so that only one implication remains. For example the uncurried
   version of @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match
-  our desired pattern @{text "_ \<Longrightarrow> C"}, and can be \emph{curried} after the
+  our desired pattern @{text "_ \<Longrightarrow> C"}, and can be \<^emph>\<open>curried\<close> after the
   match to put it back into normal form.
 \<close>