doc-src/Ref/goals.tex
changeset 8995 61e1ca01d4a3
parent 8978 894d76cbf56d
child 13479 7123ae179212
equal deleted inserted replaced
8994:803533fbb3ec 8995:61e1ca01d4a3
   365 
   365 
   366 
   366 
   367 \subsection{Timing}
   367 \subsection{Timing}
   368 \index{timing statistics}\index{proofs!timing}
   368 \index{timing statistics}\index{proofs!timing}
   369 \begin{ttbox} 
   369 \begin{ttbox} 
   370 proof_timing: bool ref \hfill{\bf initially false}
   370 timing: bool ref \hfill{\bf initially false}
   371 \end{ttbox}
   371 \end{ttbox}
   372 
   372 
   373 \begin{ttdescription}
   373 \begin{ttdescription}
   374 \item[set \ttindexbold{proof_timing};] 
   374 \item[set \ttindexbold{timing};] enables global timing in Isabelle.  In
   375 makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
   375   particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands
   376 processor time was spent.  This information is compiler-dependent.
   376   display how much processor time was spent.  This information is
       
   377   compiler-dependent.
   377 \end{ttdescription}
   378 \end{ttdescription}
   378 
   379 
   379 
   380 
   380 \section{Shortcuts for applying tactics}
   381 \section{Shortcuts for applying tactics}
   381 \index{shortcuts!for \texttt{by} commands}
   382 \index{shortcuts!for \texttt{by} commands}