renamed Syntax.trace_norm_ast to Syntax.trace_ast;
Tue, 30 May 2000 16:01:29 +0200
changeset 8996 5a5bbb6b6688
parent 8995 61e1ca01d4a3
child 8997 da290d99d8b2
renamed Syntax.trace_norm_ast to Syntax.trace_ast; removed Syntax.stat_norm_ast;
--- a/doc-src/Ref/syntax.tex	Tue May 30 16:00:55 2000 +0200
+++ b/doc-src/Ref/syntax.tex	Tue May 30 16:01:29 2000 +0200
@@ -557,15 +557,12 @@
 Normalizing an \AST{} involves repeatedly applying macro rules until
 none are applicable.  Macro rules are chosen in order of appearance in
 the theory definitions.  You can watch the normalization of \AST{}s
-during parsing and printing by setting \ttindex{Syntax.trace_norm_ast}
+during parsing and printing by setting \ttindex{Syntax.trace_ast}
 to {\tt true}.\index{tracing!of macros} Alternatively, use
 \ttindex{Syntax.test_read}.  The information displayed when tracing
 includes the \AST{} before normalization ({\tt pre}), redexes with
 results ({\tt rewrote}), the normal form finally reached ({\tt post})
-and some statistics ({\tt normalize}).  If tracing is off,
-\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to
-enable printing of the normal form and statistics only.
+and some statistics ({\tt normalize}).
 \subsection{Example: the syntax of finite sets}
 \index{examples!of macros}