changeset 16718 70c94b82c556
parent 16717 710a7a7a2b65
child 16799 978dcf30c3dd
--- a/NEWS	Wed Jul 06 10:41:51 2005 +0200
+++ b/NEWS	Wed Jul 06 20:00:20 2005 +0200
@@ -406,15 +406,15 @@
 time.  For the default print mode, both Output.output and Output.raw
 have no effect.
-* 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
-* 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: Output.time_accumulator NAME creates an operator ('a -> 'b) ->
+'a -> 'b to measure runtime and count invocations; the cumulative
+results are displayed at the end of a batch session.
+* Isar toplevel: improved diagnostics, mostly for Poly/ML only.
+Reference Toplevel.debug (default false) controls detailed printing
+and tracing of low-level exceptions; Toplevel.profiling (default 0)
+controls execution profiling -- set to 1 for time and 2 for space
+(both increase the runtime).
 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
 reasonably efficient light-weight implementation of sets as lists.
@@ -502,6 +502,8 @@
   PureThy.thms_of: theory -> (string * thm) list
   PureThy.all_thms_of: theory -> (string * thm) list
+* Pure: print_tac now outputs the goal through the trace channel.
 * Provers: Simplifier and Classical Reasoner now support proof context
 dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
 components are stored in the theory and patched into the