
diff -r 1884c40f1539 -r e467ae7aa808 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sun Oct 18 21:30:01 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sun Oct 18 22:57:09 2015 +0200
@@ -37,14 +37,14 @@
   algebra; types are qualified by ordered type classes.
 
   \<^medskip>
-  A \emph{type class} is an abstract syntactic entity
-  declared in the theory context.  The \emph{subclass relation} @{text
+  A \<^emph>\<open>type class\<close> is an abstract syntactic entity
+  declared in the theory context.  The \<^emph>\<open>subclass relation\<close> @{text
   "c\<^sub>1 \<subseteq> c\<^sub>2"} is specified by stating an acyclic
   generating relation; the transitive closure is maintained
   internally.  The resulting relation is an ordering: reflexive,
   transitive, and antisymmetric.
 
-  A \emph{sort} is a list of type classes written as @{text "s = {c\<^sub>1,
+  A \<^emph>\<open>sort\<close> is a list of type classes written as @{text "s = {c\<^sub>1,
   \<dots>, c\<^sub>m}"}, it represents symbolic intersection.  Notationally, the
   curly braces are omitted for singleton intersections, i.e.\ any
   class @{text "c"} may be read as a sort @{text "{c}"}.  The ordering
@@ -57,20 +57,20 @@
   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
+  A \<^emph>\<open>fixed type variable\<close> 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
+  A \<^emph>\<open>schematic type variable\<close> is a pair of an indexname and a
   sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually
   printed as @{text "?\<alpha>\<^sub>s"}.
 
-  Note that \emph{all} syntactic components contribute to the identity
+  Note that \<^emph>\<open>all\<close> syntactic components contribute to the identity
   of type variables: basic name, index, and sort constraint.  The core
   logic handles type variables with the same name but different sorts
   as different, although the type-inference layer (which is outside
   the core) rejects anything like that.
 
-  A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
+  A \<^emph>\<open>type constructor\<close> @{text "\<kappa>"} is a @{text "k"}-ary operator
   on types declared in the theory.  Type constructor application is
   written postfix as @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>k)\<kappa>"}.  For
   @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}
@@ -80,17 +80,17 @@
   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
   \<beta>)fun"}.
   
-  The logical category \emph{type} is defined inductively over type
+  The logical category \<^emph>\<open>type\<close> is defined inductively over type
   variables and type constructors as follows: @{text "\<tau> = \<alpha>\<^sub>s | ?\<alpha>\<^sub>s |
   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.
 
-  A \emph{type abbreviation} is a syntactic definition @{text
+  A \<^emph>\<open>type abbreviation\<close> is a syntactic definition @{text
   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations appear as type
   constructors in the syntax, but are expanded before entering the
   logical core.
 
-  A \emph{type arity} declares the image behavior of a type
+  A \<^emph>\<open>type arity\<close> declares the image behavior of a type
   constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^sub>1, \<dots>,
   s\<^sub>k)s"} means that @{text "(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"} is
   of sort @{text "s"} if every argument type @{text "\<tau>\<^sub>i"} is
@@ -99,7 +99,7 @@
   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
 
   \<^medskip>
-  The sort algebra is always maintained as \emph{coregular},
+  The sort algebra is always maintained as \<^emph>\<open>coregular\<close>,
   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> ::
@@ -238,7 +238,7 @@
   have an explicit name and type in each occurrence.
 
   \<^medskip>
-  A \emph{bound variable} is a natural number @{text "b"},
+  A \<^emph>\<open>bound variable\<close> 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
@@ -247,26 +247,26 @@
   different de-Bruijn indices at different occurrences, depending on
   the nesting of abstractions.
 
-  A \emph{loose variable} is a bound variable that is outside the
+  A \<^emph>\<open>loose variable\<close> is a bound variable that is outside the
   scope of local binders.  The types (and names) for loose variables
   can be managed as a separate context, that is maintained as a stack
   of hypothetical binders.  The core logic operates on closed terms,
   without any loose variables.
 
-  A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
+  A \<^emph>\<open>fixed variable\<close> is a pair of a basic name and a type, e.g.\
   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^sub>\<tau>"} here.  A
-  \emph{schematic variable} is a pair of an indexname and a type,
+  \<^emph>\<open>schematic variable\<close> is a pair of an indexname and a type,
   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,
+  A \<^emph>\<open>constant\<close> 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
   "c\<^sub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
 
-  The vector of \emph{type arguments} of constant @{text "c\<^sub>\<tau>"} wrt.\
+  The vector of \<^emph>\<open>type arguments\<close> of constant @{text "c\<^sub>\<tau>"} wrt.\
   the declaration @{text "c :: \<sigma>"} is defined as the codomain of the
   matcher @{text "\<vartheta> = {?\<alpha>\<^sub>1 \<mapsto> \<tau>\<^sub>1, \<dots>, ?\<alpha>\<^sub>n \<mapsto> \<tau>\<^sub>n}"} presented in
   canonical order @{text "(\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>n)"}, corresponding to the
@@ -279,14 +279,14 @@
 
   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
   for type variables in @{text "\<sigma>"}.  These are observed by
-  type-inference as expected, but \emph{ignored} by the core logic.
+  type-inference as expected, but \<^emph>\<open>ignored\<close> by the core logic.
   This means the primitive logic is able to reason with instances of
   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.
-  The logical category \emph{term} is defined inductively over atomic
+  An \<^emph>\<open>atomic term\<close> is either a variable or constant.
+  The logical category \<^emph>\<open>term\<close> 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
   converting between an external representation with named bound
@@ -303,7 +303,7 @@
   \qquad
   \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}
   \]
-  A \emph{well-typed term} is a term that can be typed according to these rules.
+  A \<^emph>\<open>well-typed term\<close> is a term that can be typed according to these rules.
 
   Typing information can be omitted: type-inference is able to
   reconstruct the most general type of a raw term, while assigning
@@ -319,7 +319,7 @@
   polymorphic constants occur routinely.
 
   \<^medskip>
-  The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
+  The \<^emph>\<open>hidden polymorphism\<close> 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,7 +328,7 @@
   pathological situation notoriously demands additional care.
 
   \<^medskip>
-  A \emph{term abbreviation} is a syntactic definition @{text
+  A \<^emph>\<open>term abbreviation\<close> 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
@@ -475,8 +475,8 @@
 section \<open>Theorems \label{sec:thms}\<close>
 
 text \<open>
-  A \emph{proposition} is a well-typed term of type @{text "prop"}, a
-  \emph{theorem} is a proven proposition (depending on a context of
+  A \<^emph>\<open>proposition\<close> is a well-typed term of type @{text "prop"}, a
+  \<^emph>\<open>theorem\<close> is a proven proposition (depending on a context of
   hypotheses and the background theory).  Primitive inferences include
   plain Natural Deduction rules for the primary connectives @{text
   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin
@@ -493,7 +493,7 @@
   derivability judgment @{text "A\<^sub>1, \<dots>, A\<^sub>n \<turnstile> B"} is
   defined inductively by the primitive inferences given in
   \figref{fig:prim-rules}, with the global restriction that the
-  hypotheses must \emph{not} contain any schematic variables.  The
+  hypotheses must \<^emph>\<open>not\<close> contain any schematic variables.  The
   builtin equality is conceptually axiomatized as shown in
   \figref{fig:pure-equality}, although the implementation works
   directly with derived inferences.
@@ -597,7 +597,7 @@
   the result belongs to a different proof context.
 
   \<^medskip>
-  An \emph{oracle} is a function that produces axioms on the
+  An \<^emph>\<open>oracle\<close> 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
@@ -608,14 +608,14 @@
   Later on, theories are usually developed in a strictly definitional
   fashion, by stating only certain equalities over new constants.
 
-  A \emph{simple definition} consists of a constant declaration @{text
+  A \<^emph>\<open>simple definition\<close> consists of a constant declaration @{text
   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t
   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS
   may depend on further defined constants, but not @{text "c"} itself.
   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>
   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.
 
-  An \emph{overloaded definition} consists of a collection of axioms
+  An \<^emph>\<open>overloaded definition\<close> consists of a collection of axioms
   for the same constant, with zero or one equations @{text
   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for
   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention
@@ -717,7 +717,7 @@
   cf.\ \secref{sec:context-theory}.
 
   \<^descr> @{ML Thm.transfer}~@{text "thy thm"} transfers the given
-  theorem to a \emph{larger} theory, see also \secref{sec:context}.
+  theorem to a \<^emph>\<open>larger\<close> theory, see also \secref{sec:context}.
   This formal adjustment of the background context has no logical
   significance, but is occasionally required for formal reasons, e.g.\
   when theorems that are imported from more basic theories are used in
@@ -920,7 +920,7 @@
   "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} cover the propositions @{text "\<Gamma>"}, @{text "\<phi>"}, as
   well as the proof of @{text "\<Gamma> \<turnstile> \<phi>"}.
 
-  These \emph{sort hypothesis} of a theorem are passed monotonically
+  These \<^emph>\<open>sort hypothesis\<close> of a theorem are passed monotonically
   through further derivations.  They are redundant, as long as the
   statement of a theorem still contains the type variables that are
   accounted here.  The logical significance of sort hypotheses is
@@ -965,7 +965,7 @@
 
 text \<open>Thanks to the inference kernel managing sort hypothesis
   according to their logical significance, this example is merely an
-  instance of \emph{ex falso quodlibet consequitur} --- not a collapse
+  instance of \<^emph>\<open>ex falso quodlibet consequitur\<close> --- not a collapse
   of the logical framework!\<close>
 
 
@@ -975,9 +975,9 @@
   The primitive inferences covered so far mostly serve foundational
   purposes.  User-level reasoning usually works via object-level rules
   that are represented as theorems of Pure.  Composition of rules
-  involves \emph{backchaining}, \emph{higher-order unification} modulo
+  involves \<^emph>\<open>backchaining\<close>, \<^emph>\<open>higher-order unification\<close> modulo
   @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called
-  \emph{lifting} of rules into a context of @{text "\<And>"} and @{text
+  \<^emph>\<open>lifting\<close> of rules into a context of @{text "\<And>"} and @{text
   "\<Longrightarrow>"} connectives.  Thus the full power of higher-order Natural
   Deduction in Isabelle/Pure becomes readily available.
 \<close>
@@ -989,7 +989,7 @@
   The idea of object-level rules is to model Natural Deduction
   inferences in the style of Gentzen @{cite "Gentzen:1935"}, but we allow
   arbitrary nesting similar to @{cite extensions91}.  The most basic
-  rule format is that of a \emph{Horn Clause}:
+  rule format is that of a \<^emph>\<open>Horn Clause\<close>:
   \[
   \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
   \]
@@ -1010,8 +1010,8 @@
 
   Nesting of rules means that the positions of @{text "A\<^sub>i"} may
   again hold compound rules, not just atomic propositions.
-  Propositions of this format are called \emph{Hereditary Harrop
-  Formulae} in the literature @{cite "Miller:1991"}.  Here we give an
+  Propositions of this format are called \<^emph>\<open>Hereditary Harrop
+  Formulae\<close> in the literature @{cite "Miller:1991"}.  Here we give an
   inductive characterization as follows:
 
   \<^medskip>
@@ -1180,7 +1180,7 @@
   logical framework.  The proof term can be inspected by a separate
   proof-checker, for example.
 
-  According to the well-known \emph{Curry-Howard isomorphism}, a proof
+  According to the well-known \<^emph>\<open>Curry-Howard isomorphism\<close>, a proof
   can be viewed as a @{text "\<lambda>"}-term. Following this idea, proofs in
   Isabelle are internally represented by a datatype similar to the one
   for terms described in \secref{sec:terms}.  On top of these
@@ -1193,9 +1193,9 @@
   polymorphism and type classes are ignored.
 
   \<^medskip>
-  \emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
+  \<^emph>\<open>Proof abstractions\<close> 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
+  "\<And>"}/@{text "\<Longrightarrow>"}, and \<^emph>\<open>proof applications\<close> of the form @{text
   "p \<cdot> t"} or @{text "p \<bullet> q"} correspond to elimination of @{text
   "\<And>"}/@{text "\<Longrightarrow>"}.  Actual types @{text "\<alpha>"}, propositions @{text
   "A"}, and terms @{text "t"} might be suppressed and reconstructed
@@ -1205,10 +1205,10 @@
   Various atomic proofs indicate special situations within
   the proof construction as follows.
 
-  A \emph{bound proof variable} is a natural number @{text "b"} that
+  A \<^emph>\<open>bound proof variable\<close> is a natural number @{text "b"} that
   acts as de-Bruijn index for proof term abstractions.
 
-  A \emph{minimal proof} ``@{text "?"}'' is a dummy proof term.  This
+  A \<^emph>\<open>minimal proof\<close> ``@{text "?"}'' is a dummy proof term.  This
   indicates some unrecorded part of the proof.
 
   @{text "Hyp A"} refers to some pending hypothesis by giving its
@@ -1216,26 +1216,26 @@
   similar to loose bound variables or free variables within a term
   (\secref{sec:terms}).
 
-  An \emph{axiom} or \emph{oracle} @{text "a : A[\<^vec>\<tau>]"} refers
+  An \<^emph>\<open>axiom\<close> or \<^emph>\<open>oracle\<close> @{text "a : A[\<^vec>\<tau>]"} refers
   some postulated @{text "proof constant"}, which is subject to
   schematic polymorphism of theory content, and the particular type
   instantiation may be given explicitly.  The vector of types @{text
   "\<^vec>\<tau>"} refers to the schematic type variables in the generic
   proposition @{text "A"} in canonical order.
 
-  A \emph{proof promise} @{text "a : A[\<^vec>\<tau>]"} is a placeholder
+  A \<^emph>\<open>proof promise\<close> @{text "a : A[\<^vec>\<tau>]"} is a placeholder
   for some proof of polymorphic proposition @{text "A"}, with explicit
   type instantiation as given by the vector @{text "\<^vec>\<tau>"}, as
   above.  Unlike axioms or oracles, proof promises may be
-  \emph{fulfilled} eventually, by substituting @{text "a"} by some
+  \<^emph>\<open>fulfilled\<close> eventually, by substituting @{text "a"} by some
   particular proof @{text "q"} at the corresponding type instance.
   This acts like Hindley-Milner @{text "let"}-polymorphism: a generic
   local proof definition may get used at different type instances, and
   is replaced by the concrete instance eventually.
 
-  A \emph{named theorem} wraps up some concrete proof as a closed
+  A \<^emph>\<open>named theorem\<close> wraps up some concrete proof as a closed
   formal entity, in the manner of constant definitions for proof
-  terms.  The \emph{proof body} of such boxed theorems involves some
+  terms.  The \<^emph>\<open>proof body\<close> of such boxed theorems involves some
   digest about oracles and promises occurring in the original proof.
   This allows the inference kernel to manage this critical information
   without the full overhead of explicit proof terms.
@@ -1247,15 +1247,15 @@
 text \<open>Fully explicit proof terms can be large, but most of this
   information is redundant and can be reconstructed from the context.
   Therefore, the Isabelle/Pure inference kernel records only
-  \emph{implicit} proof terms, by omitting all typing information in
+  \<^emph>\<open>implicit\<close> proof terms, by omitting all typing information in
   terms, all term and type labels of proof abstractions, and some
   argument terms of applications @{text "p \<cdot> t"} (if possible).
 
   There are separate operations to reconstruct the full proof term
-  later on, using \emph{higher-order pattern unification}
+  later on, using \<^emph>\<open>higher-order pattern unification\<close>
   @{cite "nipkow-patterns" and "Berghofer-Nipkow:2000:TPHOL"}.
 
-  The \emph{proof checker} expects a fully reconstructed proof term,
+  The \<^emph>\<open>proof checker\<close> expects a fully reconstructed proof term,
   and can turn it into a theorem by replaying its primitive inferences
   within the kernel.\<close>
 




