# HG changeset patch
# User wenzelm
# Date 1121263638 -7200
# Node ID 978dcf30c3dd7e6c76ce38c804de1807bdb3f10c
# Parent  36d34186741b852a8bf6e554bb7da9ddee04ab16
* Isar session: The initial use of ROOT.ML is now always timed;

diff -r 36d34186741b -r 978dcf30c3dd NEWS
--- a/NEWS	Wed Jul 13 15:25:05 2005 +0200
+++ b/NEWS	Wed Jul 13 16:07:18 2005 +0200
@@ -416,6 +416,10 @@
 controls execution profiling -- set to 1 for time and 2 for space
 (both increase the runtime).
 
+* Isar session: The initial use of ROOT.ML is now always timed,
+i.e. the log will show the actual process times, in contrast to the
+elapsed wall-clock time that the outer shell wrapper produces.
+ 
 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
 reasonably efficient light-weight implementation of sets as lists.