equal
deleted
inserted
replaced
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} |