1.1 --- a/doc-src/more_antiquote.ML	Mon Nov 10 08:18:58 2008 +0100
     1.2 +++ b/doc-src/more_antiquote.ML	Mon Nov 10 09:03:28 2008 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature MORE_ANTIQUOTE =
     1.6  sig
     1.7 -  val verbatim: string -> string
     1.8 +  val typewriter: string -> string
     1.9  end;
    1.10  
    1.11  structure More_Antiquote : MORE_ANTIQUOTE =
    1.12 @@ -15,9 +15,9 @@
    1.13  
    1.14  structure O = ThyOutput;
    1.15  
    1.16 -(* printing verbatim lines *)
    1.17 +(* printing typewriter lines *)
    1.18  
    1.19 -fun verbatim s =
    1.20 +fun typewriter s =
    1.21    let
    1.22      val parse = Scan.repeat
    1.23        (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    1.24 @@ -43,7 +43,7 @@
    1.25      val (texts, []) =  Scan.finite Symbol.stopper parse cs
    1.26    in if null texts
    1.27      then ""
    1.28 -    else implode ("\\isaverbatim%\n\\noindent%\n\\hspace*{0pt}" :: texts)
    1.29 +    else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts)
    1.30    end
    1.31  
    1.32  
    1.33 @@ -91,7 +91,7 @@
    1.34      Code_Target.code_of (ProofContext.theory_of ctxt)
    1.35        target "Example" (mk_cs (ProofContext.theory_of ctxt))
    1.36          (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
    1.37 -    |> verbatim;
    1.38 +    |> typewriter;
    1.39  
    1.40  in
    1.41