--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat May 08 19:18:28 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat May 08 19:53:11 2010 +0200
@@ -212,7 +212,6 @@
text {*
\begin{mldecls}
- @{index_ML Pretty.setdepth: "int -> unit"} \\
@{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
@{index_ML print_depth: "int -> unit"} \\
\end{mldecls}
@@ -221,12 +220,6 @@
\begin{description}
- \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to
- limit the printing depth to @{text d}. This affects the display of
- types, terms, theorems etc. The default value is 0, which permits
- printing to an arbitrary depth. Other useful values for @{text d}
- are 10 and 20.
-
\item @{ML Pretty.margin_default} indicates the global default for
the right margin of the built-in pretty printer, with initial value
76. Note that user-interfaces typically control margins