1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Nov 10 08:18:58 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Mon Nov 10 09:03:28 2008 +0100
     1.3 @@ -1114,7 +1114,7 @@
     1.4  \isatagquote
     1.5  %
     1.6  \begin{isamarkuptext}%
     1.7 -\isaverbatim%
     1.8 +\isatypewriter%
     1.9  \noindent%
    1.10  \hspace*{0pt}module Example where {\char123}\\
    1.11  \hspace*{0pt}\\
    1.12 @@ -1201,7 +1201,7 @@
    1.13  \isatagquote
    1.14  %
    1.15  \begin{isamarkuptext}%
    1.16 -\isaverbatim%
    1.17 +\isatypewriter%
    1.18  \noindent%
    1.19  \hspace*{0pt}structure Example = \\
    1.20  \hspace*{0pt}struct\\

     2.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex	Mon Nov 10 08:18:58 2008 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex	Mon Nov 10 09:03:28 2008 +0100
     2.3 @@ -24,7 +24,7 @@
     2.4  \newcommand{\qt}[1]{``{#1}''}
     2.5  
     2.6  % verbatim text
     2.7 -\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
     2.8 +\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
     2.9  
    2.10  % invisibility
    2.11  \isadroptag{theory}

     3.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Mon Nov 10 08:18:58 2008 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex	Mon Nov 10 09:03:28 2008 +0100
     3.3 @@ -262,7 +262,7 @@
     3.4  \isatagquote
     3.5  %
     3.6  \begin{isamarkuptext}%
     3.7 -\isaverbatim%
     3.8 +\isatypewriter%
     3.9  \noindent%
    3.10  \hspace*{0pt}structure Example = \\
    3.11  \hspace*{0pt}struct\\
    3.12 @@ -345,7 +345,7 @@
    3.13  \isatagquote
    3.14  %
    3.15  \begin{isamarkuptext}%
    3.16 -\isaverbatim%
    3.17 +\isatypewriter%
    3.18  \noindent%
    3.19  \hspace*{0pt}structure Example = \\
    3.20  \hspace*{0pt}struct\\
    3.21 @@ -402,7 +402,7 @@
    3.22  \isatagquote
    3.23  %
    3.24  \begin{isamarkuptext}%
    3.25 -\isaverbatim%
    3.26 +\isatypewriter%
    3.27  \noindent%
    3.28  \hspace*{0pt}structure Example = \\
    3.29  \hspace*{0pt}struct\\

     4.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Mon Nov 10 08:18:58 2008 +0100
     4.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Mon Nov 10 09:03:28 2008 +0100
     4.3 @@ -149,7 +149,7 @@
     4.4  \isatagquote
     4.5  %
     4.6  \begin{isamarkuptext}%
     4.7 -\isaverbatim%
     4.8 +\isatypewriter%
     4.9  \noindent%
    4.10  \hspace*{0pt}structure Example = \\
    4.11  \hspace*{0pt}struct\\
    4.12 @@ -228,7 +228,7 @@
    4.13  \isatagquote
    4.14  %
    4.15  \begin{isamarkuptext}%
    4.16 -\isaverbatim%
    4.17 +\isatypewriter%
    4.18  \noindent%
    4.19  \hspace*{0pt}module Example where {\char123}\\
    4.20  \hspace*{0pt}\\

     5.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Mon Nov 10 08:18:58 2008 +0100
     5.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Mon Nov 10 09:03:28 2008 +0100
     5.3 @@ -85,7 +85,7 @@
     5.4  \isatagquote
     5.5  %
     5.6  \begin{isamarkuptext}%
     5.7 -\isaverbatim%
     5.8 +\isatypewriter%
     5.9  \noindent%
    5.10  \hspace*{0pt}dequeue ::~forall a. Queue a -> (Maybe a, Queue a);\\
    5.11  \hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y, Queue xs ys);\\
    5.12 @@ -271,7 +271,7 @@
    5.13  \isatagquote
    5.14  %
    5.15  \begin{isamarkuptext}%
    5.16 -\isaverbatim%
    5.17 +\isatypewriter%
    5.18  \noindent%
    5.19  \hspace*{0pt}module Example where {\char123}\\
    5.20  \hspace*{0pt}\\
    5.21 @@ -336,7 +336,7 @@
    5.22  \isatagquote
    5.23  %
    5.24  \begin{isamarkuptext}%
    5.25 -\isaverbatim%
    5.26 +\isatypewriter%
    5.27  \noindent%
    5.28  \hspace*{0pt}structure Example = \\
    5.29  \hspace*{0pt}struct\\
    5.30 @@ -657,7 +657,7 @@
    5.31  \isatagquote
    5.32  %
    5.33  \begin{isamarkuptext}%
    5.34 -\isaverbatim%
    5.35 +\isatypewriter%
    5.36  \noindent%
    5.37  \hspace*{0pt}structure Example = \\
    5.38  \hspace*{0pt}struct\\
    5.39 @@ -774,7 +774,7 @@
    5.40  \isatagquote
    5.41  %
    5.42  \begin{isamarkuptext}%
    5.43 -\isaverbatim%
    5.44 +\isatypewriter%
    5.45  \noindent%
    5.46  \hspace*{0pt}structure Example = \\
    5.47  \hspace*{0pt}struct\\
    5.48 @@ -910,7 +910,7 @@
    5.49  \isatagquote
    5.50  %
    5.51  \begin{isamarkuptext}%
    5.52 -\isaverbatim%
    5.53 +\isatypewriter%
    5.54  \noindent%
    5.55  \hspace*{0pt}structure Example = \\
    5.56  \hspace*{0pt}struct\\
    5.57 @@ -1031,7 +1031,7 @@
    5.58  \isatagquote
    5.59  %
    5.60  \begin{isamarkuptext}%
    5.61 -\isaverbatim%
    5.62 +\isatypewriter%
    5.63  \noindent%
    5.64  \hspace*{0pt}structure Example = \\
    5.65  \hspace*{0pt}struct\\
    5.66 @@ -1106,7 +1106,7 @@
    5.67  \isatagquote
    5.68  %
    5.69  \begin{isamarkuptext}%
    5.70 -\isaverbatim%
    5.71 +\isatypewriter%
    5.72  \noindent%
    5.73  \hspace*{0pt}strict{\char95}dequeue ::~forall a. Queue a -> (a, Queue a);\\
    5.74  \hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y, Queue xs ys);\\
    5.75 @@ -1202,7 +1202,7 @@
    5.76  \isatagquote
    5.77  %
    5.78  \begin{isamarkuptext}%
    5.79 -\isaverbatim%
    5.80 +\isatypewriter%
    5.81  \noindent%
    5.82  \hspace*{0pt}empty{\char95}queue ::~forall a. a;\\
    5.83  \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\

     6.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 10 08:18:58 2008 +0100
     6.2 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 10 09:03:28 2008 +0100
     6.3 @@ -26,7 +26,7 @@
     6.4  \newcommand{\qt}[1]{``{#1}''}
     6.5  
     6.6  % verbatim text
     6.7 -\newcommand{\isaverbatim}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
     6.8 +\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
     6.9  
    6.10  % invisibility
    6.11  \isadroptag{theory}

     7.1 --- a/doc-src/more_antiquote.ML	Mon Nov 10 08:18:58 2008 +0100
     7.2 +++ b/doc-src/more_antiquote.ML	Mon Nov 10 09:03:28 2008 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  
     7.5  signature MORE_ANTIQUOTE =
     7.6  sig
     7.7 -  val verbatim: string -> string
     7.8 +  val typewriter: string -> string
     7.9  end;
    7.10  
    7.11  structure More_Antiquote : MORE_ANTIQUOTE =
    7.12 @@ -15,9 +15,9 @@
    7.13  
    7.14  structure O = ThyOutput;
    7.15  
    7.16 -(* printing verbatim lines *)
    7.17 +(* printing typewriter lines *)
    7.18  
    7.19 -fun verbatim s =
    7.20 +fun typewriter s =
    7.21    let
    7.22      val parse = Scan.repeat
    7.23        (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    7.24 @@ -43,7 +43,7 @@
    7.25      val (texts, []) =  Scan.finite Symbol.stopper parse cs
    7.26    in if null texts
    7.27      then ""
    7.28 -    else implode ("\\isaverbatim%\n\\noindent%\n\\hspace*{0pt}" :: texts)
    7.29 +    else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts)
    7.30    end
    7.31  
    7.32  
    7.33 @@ -91,7 +91,7 @@
    7.34      Code_Target.code_of (ProofContext.theory_of ctxt)
    7.35        target "Example" (mk_cs (ProofContext.theory_of ctxt))
    7.36          (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
    7.37 -    |> verbatim;
    7.38 +    |> typewriter;
    7.39  
    7.40  in
    7.41