| changeset 41377 | 390c53904220 |
| parent 41310 | 65631ca437c9 |
| child 41379 | b31d7a1cd08f |
--- a/NEWS Tue Dec 21 21:05:50 2010 +0100 +++ b/NEWS Tue Dec 21 21:21:21 2010 +0100 @@ -54,6 +54,8 @@ show_consts show_consts show_abbrevs show_abbrevs + Syntax.trace_ast syntax_ast_trace + Syntax.stat_ast syntax_ast_stat Syntax.ambiguity_level syntax_ambiguity_level Goal_Display.goals_limit goals_limit