src/Doc/Implementation/Proof.thy

 text \<open>
   Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
   is considered as ``free''.  Logically, free variables act like
   outermost universal quantification at the sequent level: @{text
   "A\<^sub>1(x), \<dots>, A\<^sub>n(x) \<turnstile> B(x)"} means that the result
-  holds \emph{for all} values of @{text "x"}.  Free variables for
+  holds \<^emph>\<open>for all\<close> values of @{text "x"}.  Free variables for
   terms (not types) can be fully internalized into the logic: @{text
   "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
   that @{text "x"} does not occur elsewhere in the context.
   Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
   quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
   while from outside it appears as a place-holder for instantiation
   (thanks to @{text "\<And>"} elimination).
 
   The Pure logic represents the idea of variables being either inside
   or outside the current scope by providing separate syntactic
-  categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
-  \emph{schematic variables} (e.g.\ @{text "?x"}).  Incidently, a
+  categories for \<^emph>\<open>fixed variables\<close> (e.g.\ @{text "x"}) vs.\
+  \<^emph>\<open>schematic variables\<close> (e.g.\ @{text "?x"}).  Incidently, a
   universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
   "\<turnstile> B(?x)"}, which represents its generality without requiring an
   explicit quantifier.  The same principle works for type variables:
   @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile> \<forall>\<alpha>. B(\<alpha>)"}''
   without demanding a truly polymorphic framework.

   would demand the context to be constructed in stages as follows:
   @{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^sub>\<alpha>)"}.
 
   We allow a slightly less formalistic mode of operation: term
   variables @{text "x"} are fixed without specifying a type yet
-  (essentially \emph{all} potential occurrences of some instance
+  (essentially \<^emph>\<open>all\<close> potential occurrences of some instance
   @{text "x\<^sub>\<tau>"} are fixed); the first occurrence of @{text "x"}
   within a specific term assigns its most general type, which is then
   maintained consistently in the context.  The above example becomes
   @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^sub>\<alpha>)"}, where type @{text
-  "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
+  "\<alpha>"} is fixed \<^emph>\<open>after\<close> term @{text "x"}, and the constraint
   @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
   @{text "x\<^sub>\<alpha>"} in the subsequent proposition.
 
   This twist of dependencies is also accommodated by the reverse
   operation of exporting results from a context: a type variable

 
 
 section \<open>Assumptions \label{sec:assumptions}\<close>
 
 text \<open>
-  An \emph{assumption} is a proposition that it is postulated in the
+  An \<^emph>\<open>assumption\<close> is a proposition that it is postulated in the
   current context.  Local conclusions may use assumptions as
   additional facts, but this imposes implicit hypotheses that weaken
   the overall statement.
 
   Assumptions are restricted to fixed non-schematic statements, i.e.\