diff -r 1884c40f1539 -r e467ae7aa808 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Sun Oct 18 21:30:01 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Sun Oct 18 22:57:09 2015 +0200
@@ -149,7 +149,7 @@
   \<close>}
 
   \<^descr> @{attribute tagged}~@{text "name value"} and @{attribute
-  untagged}~@{text name} add and remove \emph{tags} of some theorem.
+  untagged}~@{text name} add and remove \<^emph>\<open>tags\<close> of some theorem.
   Tags may be any list of string pairs that serve as formal comment.
   The first string is considered the tag name, the second its value.
   Note that @{attribute untagged} removes any tags of the same name.
@@ -395,7 +395,7 @@
 
 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
 
-text \<open>The above attempt \emph{fails}, because @{term "0"} and @{term
+text \<open>The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term
   "op +"} in the HOL library are declared as generic type class
   operations, without stating any algebraic laws yet.  More specific
   types are required to get access to certain standard simplifications
@@ -586,7 +586,7 @@
   @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
     (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}
 
-  A congruence rule can also \emph{prevent} simplification of some
+  A congruence rule can also \<^emph>\<open>prevent\<close> simplification of some
   arguments.  Here is an alternative congruence rule for conditional
   expressions that conforms to non-strict functional evaluation:
   @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
@@ -617,7 +617,7 @@
   point.  Also note that definitional packages like @{command
   "datatype"}, @{command "primrec"}, @{command "fun"} routinely
   declare Simplifier rules to the target context, while plain
-  @{command "definition"} is an exception in \emph{not} declaring
+  @{command "definition"} is an exception in \<^emph>\<open>not\<close> declaring
   anything.
 
   \<^medskip>
@@ -647,7 +647,7 @@
 
 subsection \<open>Ordered rewriting with permutative rules\<close>
 
-text \<open>A rewrite rule is \emph{permutative} if the left-hand side and
+text \<open>A rewrite rule is \<^emph>\<open>permutative\<close> if the left-hand side and
   right-hand side are the equal up to renaming of variables.  The most
   common permutative rule is commutativity: @{text "?x + ?y = ?y +
   ?x"}.  Other examples include @{text "(?x - ?y) - ?z = (?x - ?z) -
@@ -656,7 +656,7 @@
   special attention.
 
   Because ordinary rewriting loops given such rules, the Simplifier
-  employs a special strategy, called \emph{ordered rewriting}.
+  employs a special strategy, called \<^emph>\<open>ordered rewriting\<close>.
   Permutative rules are detected and only applied if the rewriting
   step decreases the redex wrt.\ a given term ordering.  For example,
   commutativity rewrites @{text "b + a"} to @{text "a + b"}, but then
@@ -688,7 +688,7 @@
 
   \<^item> To complete your set of rewrite rules, you must add not just
   associativity (A) and commutativity (C) but also a derived rule
-  \emph{left-commutativity} (LC): @{text "f x (f y z) = f y (f x z)"}.
+  \<^emph>\<open>left-commutativity\<close> (LC): @{text "f x (f y z) = f y (f x z)"}.
 
 
   Ordered rewriting with the combination of A, C, and LC sorts a term
@@ -818,7 +818,7 @@
   Any successful result needs to be a (possibly conditional) rewrite
   rule @{text "t \<equiv> u"} that is applicable to the current redex.  The
   rule will be applied just as any ordinary rewrite rule.  It is
-  expected to be already in \emph{internal form}, bypassing the
+  expected to be already in \<^emph>\<open>internal form\<close>, bypassing the
   automatic preprocessing of object-level equivalences.
 
   \begin{matharray}{rcl}
@@ -1027,7 +1027,7 @@
   \begin{warn}
   If a premise of a congruence rule cannot be proved, then the
   congruence is ignored.  This should only happen if the rule is
-  \emph{conditional} --- that is, contains premises not of the form
+  \<^emph>\<open>conditional\<close> --- that is, contains premises not of the form
   @{text "t = ?x"}.  Otherwise it indicates that some congruence rule,
   or possibly the subgoaler or solver, is faulty.
   \end{warn}
@@ -1054,7 +1054,7 @@
   all over again.  Each of the subgoals generated by the looper is
   attacked in turn, in reverse order.
 
-  A typical looper is \emph{case splitting}: the expansion of a
+  A typical looper is \<^emph>\<open>case splitting\<close>: the expansion of a
   conditional.  Another possibility is to apply an elimination rule on
   the assumptions.  More adventurous loopers could start an induction.
 
@@ -1138,7 +1138,7 @@
 
   Note that forward simplification restricts the Simplifier to its
   most basic operation of term rewriting; solver and looper tactics
-  (\secref{sec:simp-strategies}) are \emph{not} involved here.  The
+  (\secref{sec:simp-strategies}) are \<^emph>\<open>not\<close> involved here.  The
   @{attribute simplified} attribute should be only rarely required
   under normal circumstances.
 \<close>
@@ -1183,21 +1183,21 @@
   interactive proof.  But natural deduction does not easily lend
   itself to automation, and has a bias towards intuitionism.  For
   certain proofs in classical logic, it can not be called natural.
-  The \emph{sequent calculus}, a generalization of natural deduction,
+  The \<^emph>\<open>sequent calculus\<close>, a generalization of natural deduction,
   is easier to automate.
 
-  A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}
+  A \<^bold>\<open>sequent\<close> has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"}
   and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order
   logic, sequents can equivalently be made from lists or multisets of
   formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is
-  \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>
+  \<^bold>\<open>valid\<close> if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or>
   Q\<^sub>n"}.  Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which
   is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals.  A
-  sequent is \textbf{basic} if its left and right sides have a common
+  sequent is \<^bold>\<open>basic\<close> if its left and right sides have a common
   formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially
   valid.
 
-  Sequent rules are classified as \textbf{right} or \textbf{left},
+  Sequent rules are classified as \<^bold>\<open>right\<close> or \<^bold>\<open>left\<close>,
   indicating which side of the @{text "\<turnstile>"} symbol they operate on.
   Rules that operate on the right side are analogous to natural
   deduction's introduction rules, and left rules are analogous to
@@ -1341,8 +1341,8 @@
 
 text \<open>The proof tools of the Classical Reasoner depend on
   collections of rules declared in the context, which are classified
-  as introduction, elimination or destruction and as \emph{safe} or
-  \emph{unsafe}.  In general, safe rules can be attempted blindly,
+  as introduction, elimination or destruction and as \<^emph>\<open>safe\<close> or
+  \<^emph>\<open>unsafe\<close>.  In general, safe rules can be attempted blindly,
   while unsafe rules must be used with care.  A safe rule must never
   reduce a provable goal to an unprovable set of subgoals.
 
@@ -1393,9 +1393,9 @@
 
   \<^descr> @{attribute intro}, @{attribute elim}, and @{attribute dest}
   declare introduction, elimination, and destruction rules,
-  respectively.  By default, rules are considered as \emph{unsafe}
+  respectively.  By default, rules are considered as \<^emph>\<open>unsafe\<close>
   (i.e.\ not applied blindly without backtracking), while ``@{text
-  "!"}'' classifies as \emph{safe}.  Rule declarations marked by
+  "!"}'' classifies as \<^emph>\<open>safe\<close>.  Rule declarations marked by
   ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
   \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
   of the @{method rule} method).  The optional natural number
@@ -1702,7 +1702,7 @@
 
   The classical reasoning tools --- except @{method blast} --- allow
   to modify this basic proof strategy by applying two lists of
-  arbitrary \emph{wrapper tacticals} to it.  The first wrapper list,
+  arbitrary \<^emph>\<open>wrapper tacticals\<close> to it.  The first wrapper list,
   which is considered to contain safe wrappers only, affects @{method
   safe_step} and all the tactics that call it.  The second one, which
   may contain unsafe wrappers, affects the unsafe parts of @{method
@@ -1723,7 +1723,7 @@
   tactic.
 
   \<^descr> @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a
-  safe wrapper, such that it is tried \emph{before} each safe step of
+  safe wrapper, such that it is tried \<^emph>\<open>before\<close> each safe step of
   the search.
 
   \<^descr> @{text "ctxt addSafter (name, tac)"} adds the given tactic as a
@@ -1738,10 +1738,10 @@
 
   \<^descr> @{text "ctxt addbefore (name, tac)"} adds the given tactic as an
   unsafe wrapper, such that it its result is concatenated
-  \emph{before} the result of each unsafe step.
+  \<^emph>\<open>before\<close> the result of each unsafe step.
 
   \<^descr> @{text "ctxt addafter (name, tac)"} adds the given tactic as an
-  unsafe wrapper, such that it its result is concatenated \emph{after}
+  unsafe wrapper, such that it its result is concatenated \<^emph>\<open>after\<close>
   the result of each unsafe step.
 
   \<^descr> @{text "ctxt delWrapper name"} deletes the unsafe wrapper with