# HG changeset patch
# User wenzelm
# Date 959695255 -7200
# Node ID 61e1ca01d4a375e03fe3079e3aefaa0170d049f0
# Parent  803533fbb3ec5d6eb11f38c55cb5b9f7737e493a
proof_timing replaced by global timing;

diff -r 803533fbb3ec -r 61e1ca01d4a3 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Tue May 30 16:00:19 2000 +0200
+++ b/doc-src/Ref/goals.tex	Tue May 30 16:00:55 2000 +0200
@@ -367,13 +367,14 @@
 \subsection{Timing}
 \index{timing statistics}\index{proofs!timing}
 \begin{ttbox} 
-proof_timing: bool ref \hfill{\bf initially false}
+timing: bool ref \hfill{\bf initially false}
 \end{ttbox}
 
 \begin{ttdescription}
-\item[set \ttindexbold{proof_timing};] 
-makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
-processor time was spent.  This information is compiler-dependent.
+\item[set \ttindexbold{timing};] enables global timing in Isabelle.  In
+  particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands
+  display how much processor time was spent.  This information is
+  compiler-dependent.
 \end{ttdescription}