SYNC;
authorwenzelm
Fri, 21 Nov 1997 15:40:56 +0100
changeset 4275 349754bdd5b7
parent 4274 2048e7a79d09
child 4276 a770eae2cdb0
SYNC;
doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Fri Nov 21 15:37:02 1997 +0100
+++ b/doc-src/Ref/ref.ind	Fri Nov 21 15:40:56 1997 +0100
@@ -437,7 +437,7 @@
   \item {\tt prems_of}, \bold{39}
   \item {\tt prems_of_ss}, 105
   \item pretty printing, 70, 72--73, 89
-  \item {\tt Pretty.setdepth}, \bold{3}
+  \item {\tt Pretty.setdepth}, \bold{4}
   \item {\tt Pretty.setmargin}, \bold{4}
   \item {\tt PRIMITIVE}, \bold{25}
   \item {\tt primrec}, 100
@@ -570,7 +570,7 @@
   \item search, 28
     \subitem tacticals, 30--32
   \item {\tt SELECT_GOAL}, 20, \bold{33}
-  \item {\tt Sequence.seq} ML type, 25
+  \item {\tt Seq.seq} ML type, 25
   \item sequences (lazy lists), \bold{26}
   \item sequent calculus, 119
   \item sessions, 1--5