# HG changeset patch
# User wenzelm
# Date 1120222505 -7200
# Node ID 0836569a8ffcc50a5b59a3598b96de5a8a88ee5f
# Parent  507438b27f66c428c345482b0ab8efd8986e029f
* Isar profiling: new reference Toplevel.profiling (default 0);

diff -r 507438b27f66 -r 0836569a8ffc NEWS
--- a/NEWS	Fri Jul 01 14:42:05 2005 +0200
+++ b/NEWS	Fri Jul 01 14:55:05 2005 +0200
@@ -407,8 +407,13 @@
 
 * Pure: print_tac now outputs the goal through the trace channel.
 
-* Isar debugging: new reference Toplevel.debug; default false.  Set to
-make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
+* Isar debugging: new reference Toplevel.debug (default false).  Set
+to make printing of exceptions THM, TERM, TYPE and THEORY more
+verbose.
+
+* Isar profiling: new reference Toplevel.profiling (default 0).  For
+Poly/ML, set to 1 to profile time, 2 to profile space (which increases
+the runtime).
 
 * Pure: name spaces have been refined, with significant changes of the
 internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)