equal
deleted
inserted
replaced
69 by running |
69 by running |
70 \begin{ttbox} |
70 \begin{ttbox} |
71 isabelle Foo |
71 isabelle Foo |
72 \end{ttbox} |
72 \end{ttbox} |
73 |
73 |
74 More details about the \texttt{isabelle} command may be found in the |
74 More details about the \texttt{isabelle} command may be found in \emph{The |
75 \emph{System Manual}. |
75 Isabelle System Manual}. |
76 |
76 |
77 \medskip Saving the state is not enough. Record, on a file, the |
77 \medskip Saving the state is not enough. Record, on a file, the |
78 top-level commands that generate your theories and proofs. Such a |
78 top-level commands that generate your theories and proofs. Such a |
79 record allows you to replay the proofs whenever required, for instance |
79 record allows you to replay the proofs whenever required, for instance |
80 after making minor changes to the axioms. Ideally, your record will |
80 after making minor changes to the axioms. Ideally, your record will |
133 |
133 |
134 \item[\ttindexbold{time_use} "$file$";] |
134 \item[\ttindexbold{time_use} "$file$";] |
135 performs {\tt use~"$file$"} and prints the total execution time. |
135 performs {\tt use~"$file$"} and prints the total execution time. |
136 \end{ttdescription} |
136 \end{ttdescription} |
137 |
137 |
138 The $dir$ and $file$ specifications of the \texttt{cd} and |
138 The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use} |
139 \texttt{use} commands may contain path variables that are expanded |
139 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are |
140 appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax} |
140 expanded appropriately. Note that \texttt{\~\relax} abbreviates |
141 (which abbreviates \texttt{\$HOME}). Section~\ref{LoadingTheories} |
141 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates |
142 describes commands for loading theory files. |
142 \texttt{\$ISABELLE_HOME}. Section~\ref{LoadingTheories} describes commands |
|
143 for loading theory files. |
143 |
144 |
144 |
145 |
145 \section{Setting flags} |
146 \section{Setting flags} |
146 \begin{ttbox} |
147 \begin{ttbox} |
147 set : bool ref -> bool |
148 set : bool ref -> bool |
187 \subsection{Printing of hypotheses, brackets, types etc.} |
188 \subsection{Printing of hypotheses, brackets, types etc.} |
188 \index{meta-assumptions!printing of} |
189 \index{meta-assumptions!printing of} |
189 \index{types!printing of}\index{sorts!printing of} |
190 \index{types!printing of}\index{sorts!printing of} |
190 \begin{ttbox} |
191 \begin{ttbox} |
191 show_hyps : bool ref \hfill{\bf initially true} |
192 show_hyps : bool ref \hfill{\bf initially true} |
|
193 show_tags : bool ref \hfill{\bf initially false} |
192 show_brackets : bool ref \hfill{\bf initially false} |
194 show_brackets : bool ref \hfill{\bf initially false} |
193 show_types : bool ref \hfill{\bf initially false} |
195 show_types : bool ref \hfill{\bf initially false} |
194 show_sorts : bool ref \hfill{\bf initially false} |
196 show_sorts : bool ref \hfill{\bf initially false} |
195 show_consts : bool ref \hfill{\bf initially false} |
197 show_consts : bool ref \hfill{\bf initially false} |
196 long_names : bool ref \hfill{\bf initially false} |
198 long_names : bool ref \hfill{\bf initially false} |
206 |
208 |
207 \begin{ttdescription} |
209 \begin{ttdescription} |
208 |
210 |
209 \item[reset \ttindexbold{show_hyps};] makes Isabelle show each |
211 \item[reset \ttindexbold{show_hyps};] makes Isabelle show each |
210 meta-level hypothesis as a dot. |
212 meta-level hypothesis as a dot. |
|
213 |
|
214 \item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems |
|
215 (which are basically just comments that may be attached by some tools). |
211 |
216 |
212 \item[set \ttindexbold{show_brackets};] makes Isabelle show full |
217 \item[set \ttindexbold{show_brackets};] makes Isabelle show full |
213 bracketing. In particular, this reveals the grouping of infix |
218 bracketing. In particular, this reveals the grouping of infix |
214 operators. |
219 operators. |
215 |
220 |