summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 30 May 2000 16:00:55 +0200 | |

changeset 8995 | 61e1ca01d4a3 |

parent 8994 | 803533fbb3ec |

child 8996 | 5a5bbb6b6688 |

proof_timing replaced by global timing;

--- 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}