diff -r 55e73b352287 -r b9a3324e4e62 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Mon Oct 12 20:42:20 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Mon Oct 12 20:58:58 2015 +0200
@@ -36,7 +36,8 @@
   The language of types is an uninterpreted order-sorted first-order
   algebra; types are qualified by ordered type classes.
 
-  \medskip A \emph{type class} is an abstract syntactic entity
+  \<^medskip>
+  A \emph{type class} is an abstract syntactic entity
   declared in the theory context.  The \emph{subclass relation} @{text
   "c\<^sub>1 \<subseteq> c\<^sub>2"} is specified by stating an acyclic
   generating relation; the transitive closure is maintained
@@ -55,7 +56,8 @@
   empty one!  The intersection of all (finitely many) classes declared
   in the current theory is the least element wrt.\ the sort ordering.
 
-  \medskip A \emph{fixed type variable} is a pair of a basic name
+  \<^medskip>
+  A \emph{fixed type variable} is a pair of a basic name
   (starting with a @{text "'"} character) and a sort constraint, e.g.\
   @{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^sub>s"}.
   A \emph{schematic type variable} is a pair of an indexname and a
@@ -96,7 +98,8 @@
   completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
 
-  \medskip The sort algebra is always maintained as \emph{coregular},
+  \<^medskip>
+  The sort algebra is always maintained as \emph{coregular},
   which means that type arities are consistent with the subclass
   relation: for any type constructor @{text "\<kappa>"}, and classes @{text
   "c\<^sub>1 \<subseteq> c\<^sub>2"}, and arities @{text "\<kappa> ::
@@ -242,7 +245,8 @@
   corresponding binders.  In contrast, free variables and constants
   have an explicit name and type in each occurrence.
 
-  \medskip A \emph{bound variable} is a natural number @{text "b"},
+  \<^medskip>
+  A \emph{bound variable} is a natural number @{text "b"},
   which accounts for the number of intermediate binders between the
   variable occurrence in the body and its binding position.  For
   example, the de-Bruijn term @{text "\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0"} would
@@ -263,7 +267,8 @@
   e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text
   "?x\<^sub>\<tau>"}.
 
-  \medskip A \emph{constant} is a pair of a basic name and a type,
+  \<^medskip>
+  A \emph{constant} is a pair of a basic name and a type,
   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^sub>\<tau>"}
   here.  Constants are declared in the context as polymorphic families
   @{text "c :: \<sigma>"}, meaning that all substitution instances @{text
@@ -287,7 +292,8 @@
   polymorphic constants that the user-level type-checker would reject
   due to violation of type class restrictions.
 
-  \medskip An \emph{atomic term} is either a variable or constant.
+  \<^medskip>
+  An \emph{atomic term} is either a variable or constant.
   The logical category \emph{term} is defined inductively over atomic
   terms, with abstraction and application as follows: @{text "t = b |
   x\<^sub>\<tau> | ?x\<^sub>\<tau> | c\<^sub>\<tau> | \<lambda>\<^sub>\<tau>. t | t\<^sub>1 t\<^sub>2"}.  Parsing and printing takes care of
@@ -320,7 +326,8 @@
   name, but different types.  In contrast, mixed instances of
   polymorphic constants occur routinely.
 
-  \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
+  \<^medskip>
+  The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
   is the set of type variables occurring in @{text "t"}, but not in
   its type @{text "\<sigma>"}.  This means that the term implicitly depends
   on type arguments that are not accounted in the result type, i.e.\
@@ -328,14 +335,16 @@
   @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
   pathological situation notoriously demands additional care.
 
-  \medskip A \emph{term abbreviation} is a syntactic definition @{text
+  \<^medskip>
+  A \emph{term abbreviation} is a syntactic definition @{text
   "c\<^sub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},
   without any hidden polymorphism.  A term abbreviation looks like a
   constant in the syntax, but is expanded before entering the logical
   core.  Abbreviations are usually reverted when printing terms, using
   @{text "t \<rightarrow> c\<^sub>\<sigma>"} as rules for higher-order rewriting.
 
-  \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
+  \<^medskip>
+  Canonical operations on @{text "\<lambda>"}-terms include @{text
   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free
   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
   abstraction applied to an argument term, substituting the argument
@@ -569,7 +578,8 @@
   the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses
   @{text "x : A"} are treated uniformly for propositions and types.}
 
-  \medskip The axiomatization of a theory is implicitly closed by
+  \<^medskip>
+  The axiomatization of a theory is implicitly closed by
   forming all instances of type and term variables: @{text "\<turnstile>
   A\<vartheta>"} holds for any substitution instance of an axiom
   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
@@ -602,7 +612,8 @@
   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:
   the result belongs to a different proof context.
 
-  \medskip An \emph{oracle} is a function that produces axioms on the
+  \<^medskip>
+  An \emph{oracle} is a function that produces axioms on the
   fly.  Logically, this is an instance of the @{text "axiom"} rule
   (\figref{fig:prim-rules}), but there is an operational difference.
   The system always records oracle invocations within derivations of
@@ -1036,13 +1047,13 @@
   Formulae} in the literature @{cite "Miller:1991"}.  Here we give an
   inductive characterization as follows:
 
-  \medskip
+  \<^medskip>
   \begin{tabular}{ll}
   @{text "\<^bold>x"} & set of variables \\
   @{text "\<^bold>A"} & set of atomic propositions \\
   @{text "\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\
   \end{tabular}
-  \medskip
+  \<^medskip>
 
   Thus we essentially impose nesting levels on propositions formed
   from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a prefix
@@ -1054,17 +1065,18 @@
   already marks the limit of rule complexity that is usually seen in
   practice.
 
-  \medskip Regular user-level inferences in Isabelle/Pure always
+  \<^medskip>
+  Regular user-level inferences in Isabelle/Pure always
   maintain the following canonical form of results:
 
   \begin{itemize}
 
-  \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},
+  \<^item> Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},
   which is a theorem of Pure, means that quantifiers are pushed in
   front of implication at each level of nesting.  The normal form is a
   Hereditary Harrop Formula.
 
-  \item The outermost prefix of parameters is represented via
+  \<^item> The outermost prefix of parameters is represented via
   schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x
   \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.
   Note that this representation looses information about the order of
@@ -1225,7 +1237,8 @@
   @{cite "Barendregt-Geuvers:2001"}, if some fine points like schematic
   polymorphism and type classes are ignored.
 
-  \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
+  \<^medskip>
+  \emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
   or @{text "\<^bold>\<lambda>p : A. prf"} correspond to introduction of @{text
   "\<And>"}/@{text "\<Longrightarrow>"}, and \emph{proof applications} of the form @{text
   "p \<cdot> t"} or @{text "p \<bullet> q"} correspond to elimination of @{text
@@ -1233,7 +1246,8 @@
   "A"}, and terms @{text "t"} might be suppressed and reconstructed
   from the overall proof term.
 
-  \medskip Various atomic proofs indicate special situations within
+  \<^medskip>
+  Various atomic proofs indicate special situations within
   the proof construction as follows.
 
   A \emph{bound proof variable} is a natural number @{text "b"} that
@@ -1326,7 +1340,8 @@
   using @{text "p \<cdot> TYPE(type)"} (they must appear before any other
   term argument of a theorem or axiom, but may be omitted altogether).
 
-  \medskip There are separate read and print operations for proof
+  \<^medskip>
+  There are separate read and print operations for proof
   terms, in order to avoid conflicts with the regular term language.
 \<close>
 
@@ -1436,7 +1451,8 @@
   recursively explores the graph of the proofs of all theorems being
   used here.
 
-  \medskip Alternatively, we may produce a proof term manually, and
+  \<^medskip>
+  Alternatively, we may produce a proof term manually, and
   turn it into a theorem as follows:\<close>
 
 ML_val \<open>
@@ -1454,7 +1470,9 @@
     |> Drule.export_without_context;
 \<close>
 
-text \<open>\medskip See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"}
+text \<open>
+  \<^medskip>
+  See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"}
   for further examples, with export and import of proof terms via
   XML/ML data representation.
 \<close>