# HG changeset patch
# User wenzelm
# Date 1446842942 -3600
# Node ID 810486f886bf06432c8906ca0df731d4f91f8a5b
# Parent  d80eb8f6eb47a5166127f77ddf139f01f5f11b7c
more antiquotations;

diff -r d80eb8f6eb47 -r 810486f886bf src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Fri Nov 06 19:46:00 2015 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Fri Nov 06 21:49:02 2015 +0100
@@ -112,7 +112,7 @@
   macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
   few predefined control symbols, such as \verb,\,\verb,<^sub>, and
   \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
-  printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
+  printable symbol, respectively.  For example, \<^verbatim>\<open>A\<^sup>\<star>\<close>, is
   output as @{text "A\<^sup>\<star>"}.
 
   A number of symbols are considered letters by the Isabelle lexer and
@@ -125,7 +125,7 @@
   in the trailing part of an identifier. This means that the input
 
   \medskip
-  {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^sub>1.,~\verb,\,\verb,<alpha>\<^sub>1 = \,\verb,<Pi>\<^sub>\<A>,}
+  {\small\noindent \<^verbatim>\<open>\<forall>\<alpha>\<^sub>1. \<alpha>\<^sub>1 = \<Pi>\<^sub>\<A>\<close>}
 
   \medskip
   \noindent is recognized as the term @{term "\<forall>\<alpha>\<^sub>1. \<alpha>\<^sub>1 = \<Pi>\<^sub>\<A>"}