# HG changeset patch
# User wenzelm
# Date 1444674694 -7200
# Node ID 0d2d399c90a41456d4b784450d01e7b2aa4d3737
# Parent  6d892287d0e90ffcb881d9d4c6d64abf11c61884
more antiquotations;

diff -r 6d892287d0e9 -r 0d2d399c90a4 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Oct 12 20:25:50 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Oct 12 20:31:34 2015 +0200
@@ -516,9 +516,9 @@
   Instances have an optional qualifier which applies to names in
   declarations.  Names include local definitions and theorem names.
   If present, the qualifier itself is either optional
-  (``\texttt{?}''), which means that it may be omitted on input of the
-  qualified name, or mandatory (``\texttt{!}'').  If neither
-  ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
+  (``@{verbatim "?"}''), which means that it may be omitted on input of the
+  qualified name, or mandatory (``@{verbatim "!"}'').  If neither
+  ``@{verbatim "?"}'' nor ``@{verbatim "!"}'' are present, the command's default
   is used.  For @{command "interpretation"} and @{command "interpret"}
   the default is ``mandatory'', for @{command "locale"} and @{command
   "sublocale"} the default is ``optional''.  Qualifiers play no role
diff -r 6d892287d0e9 -r 0d2d399c90a4 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Oct 12 20:25:50 2015 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Oct 12 20:31:34 2015 +0200
@@ -270,7 +270,7 @@
   images.  Accordingly, it runs instances of the prover process with
   optional document preparation.  Its command-line usage
   is:\footnote{Isabelle/Scala provides the same functionality via
-  \texttt{isabelle.Build.build}.}
+  @{verbatim "isabelle.Build.build"}.}
   @{verbatim [display]
 \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
@@ -307,7 +307,7 @@
   component directories (\secref{sec:components}), augmented by more
   directories given via options @{verbatim "-d"}~@{text "DIR"} on the
   command line.  Each such directory may contain a session
-  \texttt{ROOT} file with several session specifications.
+  @{verbatim ROOT} file with several session specifications.
 
   Any session root directory may refer recursively to further
   directories of the same kind, by listing them in a catalog file
@@ -347,7 +347,7 @@
   (\secref{sec:system-options}) that are passed to the prover
   eventually.  The settings variable @{setting_ref
   ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
-  \texttt{ISABELLE_BUILD_OPTIONS="document=pdf threads=4"}. Moreover,
+  @{verbatim \<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>}. Moreover,
   the environment of system build options may be augmented on the
   command line via @{verbatim "-o"}~@{text "name"}@{verbatim
   "="}@{text "value"} or @{verbatim "-o"}~@{text "name"}, which