src/Doc/Isar_Ref/Proof_Script.thy

 
 chapter \<open>Proof scripts\<close>
 
 text \<open>
   Interactive theorem proving is traditionally associated with ``proof
-  scripts'', but Isabelle/Isar is centered around structured \emph{proof
-  documents} instead (see also \chref{ch:proofs}).
+  scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof
+  documents\<close> instead (see also \chref{ch:proofs}).
 
   Nonetheless, it is possible to emulate proof scripts by sequential
   refinements of a proof state in backwards mode, notably with the @{command
   apply} command (see \secref{sec:tactic-commands}). There are also various
   proof methods that allow to refer to implicit goal state information that

   initial position, but unlike @{command "proof"} it retains ``@{text
   "proof(prove)"}'' mode.  Thus consecutive method applications may be
   given just as in tactic scripts.
 
   Facts are passed to @{text m} as indicated by the goal's
-  forward-chain mode, and are \emph{consumed} afterwards.  Thus any
+  forward-chain mode, and are \<^emph>\<open>consumed\<close> afterwards.  Thus any
   further @{command "apply"} command would always work in a purely
   backward manner.
 
   \<^descr> @{command "apply_end"}~@{text "m"} applies proof method @{text
   m} as if in terminal position.  Basically, this simulates a

   structured proofs, but the text of the parameters, premises and conclusion
   is not given explicitly.
 
   Goal parameters may be specified separately, in order to allow referring
   to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x
-  y z"}'' names a \emph{prefix}, and ``@{command subgoal}~@{keyword
-  "for"}~@{text "\<dots> x y z"}'' names a \emph{suffix} of goal parameters. The
+  y z"}'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
+  "for"}~@{text "\<dots> x y z"}'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
   latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
   positions may be skipped via dummies (underscore). Unspecified names
   remain internal, and thus inaccessible in the proof text.
 
   ``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that

   @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
   as new subgoals (in the original context).
 
   \<^descr> @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
-  \emph{suffix} of variables.
+  \<^emph>\<open>suffix\<close> of variables.
 
   \<^descr> @{method rotate_tac}~@{text n} rotates the premises of a
   subgoal by @{text n} positions: from right to left if @{text n} is
   positive, and from left to right if @{text n} is negative; the
   default value is 1.