41 |
41 |
42 modes: '(' (name + ) ')' |
42 modes: '(' (name + ) ')' |
43 ; |
43 ; |
44 \end{rail} |
44 \end{rail} |
45 |
45 |
46 \begin{descr} |
46 \begin{description} |
47 |
47 |
48 \item [@{command "pr"}~@{text "goals, prems"}] prints the current |
48 \item @{command "pr"}~@{text "goals, prems"} prints the current |
49 proof state (if present), including the proof context, current facts |
49 proof state (if present), including the proof context, current facts |
50 and goals. The optional limit arguments affect the number of goals |
50 and goals. The optional limit arguments affect the number of goals |
51 and premises to be displayed, which is initially 10 for both. |
51 and premises to be displayed, which is initially 10 for both. |
52 Omitting limit values leaves the current setting unchanged. |
52 Omitting limit values leaves the current setting unchanged. |
53 |
53 |
54 \item [@{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] retrieves |
54 \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves |
55 theorems from the current theory or proof context. Note that any |
55 theorems from the current theory or proof context. Note that any |
56 attributes included in the theorem specifications are applied to a |
56 attributes included in the theorem specifications are applied to a |
57 temporary context derived from the current theory or proof; the |
57 temporary context derived from the current theory or proof; the |
58 result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, |
58 result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, |
59 \<dots>, a\<^sub>n"} do not have any permanent effect. |
59 \<dots>, a\<^sub>n"} do not have any permanent effect. |
60 |
60 |
61 \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}] |
61 \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>} |
62 read, type-check and print terms or propositions according to the |
62 read, type-check and print terms or propositions according to the |
63 current theory or proof context; the inferred type of @{text t} is |
63 current theory or proof context; the inferred type of @{text t} is |
64 output as well. Note that these commands are also useful in |
64 output as well. Note that these commands are also useful in |
65 inspecting the current environment of term abbreviations. |
65 inspecting the current environment of term abbreviations. |
66 |
66 |
67 \item [@{command "typ"}~@{text \<tau>}] reads and prints types of the |
67 \item @{command "typ"}~@{text \<tau>} reads and prints types of the |
68 meta-logic according to the current theory or proof context. |
68 meta-logic according to the current theory or proof context. |
69 |
69 |
70 \item [@{command "prf"}] displays the (compact) proof term of the |
70 \item @{command "prf"} displays the (compact) proof term of the |
71 current proof state (if present), or of the given theorems. Note |
71 current proof state (if present), or of the given theorems. Note |
72 that this requires proof terms to be switched on for the current |
72 that this requires proof terms to be switched on for the current |
73 object logic (see the ``Proof terms'' section of the Isabelle |
73 object logic (see the ``Proof terms'' section of the Isabelle |
74 reference manual for information on how to do this). |
74 reference manual for information on how to do this). |
75 |
75 |
76 \item [@{command "full_prf"}] is like @{command "prf"}, but displays |
76 \item @{command "full_prf"} is like @{command "prf"}, but displays |
77 the full proof term, i.e.\ also displays information omitted in the |
77 the full proof term, i.e.\ also displays information omitted in the |
78 compact proof term, which is denoted by ``@{text _}'' placeholders |
78 compact proof term, which is denoted by ``@{text _}'' placeholders |
79 there. |
79 there. |
80 |
80 |
81 \end{descr} |
81 \end{description} |
82 |
82 |
83 All of the diagnostic commands above admit a list of @{text modes} |
83 All of the diagnostic commands above admit a list of @{text modes} |
84 to be specified, which is appended to the current print mode (see |
84 to be specified, which is appended to the current print mode (see |
85 also \cite{isabelle-ref}). Thus the output behavior may be modified |
85 also \cite{isabelle-ref}). Thus the output behavior may be modified |
86 according particular print mode features. For example, @{command |
86 according particular print mode features. For example, @{command |
126 |
126 |
127 These commands print certain parts of the theory and proof context. |
127 These commands print certain parts of the theory and proof context. |
128 Note that there are some further ones available, such as for the set |
128 Note that there are some further ones available, such as for the set |
129 of rules declared for simplifications. |
129 of rules declared for simplifications. |
130 |
130 |
131 \begin{descr} |
131 \begin{description} |
132 |
132 |
133 \item [@{command "print_commands"}] prints Isabelle's outer theory |
133 \item @{command "print_commands"} prints Isabelle's outer theory |
134 syntax, including keywords and command. |
134 syntax, including keywords and command. |
135 |
135 |
136 \item [@{command "print_theory"}] prints the main logical content of |
136 \item @{command "print_theory"} prints the main logical content of |
137 the theory context; the ``@{text "!"}'' option indicates extra |
137 the theory context; the ``@{text "!"}'' option indicates extra |
138 verbosity. |
138 verbosity. |
139 |
139 |
140 \item [@{command "print_syntax"}] prints the inner syntax of types |
140 \item @{command "print_syntax"} prints the inner syntax of types |
141 and terms, depending on the current context. The output can be very |
141 and terms, depending on the current context. The output can be very |
142 verbose, including grammar tables and syntax translation rules. See |
142 verbose, including grammar tables and syntax translation rules. See |
143 \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's |
143 \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's |
144 inner syntax. |
144 inner syntax. |
145 |
145 |
146 \item [@{command "print_methods"}] prints all proof methods |
146 \item @{command "print_methods"} prints all proof methods |
147 available in the current theory context. |
147 available in the current theory context. |
148 |
148 |
149 \item [@{command "print_attributes"}] prints all attributes |
149 \item @{command "print_attributes"} prints all attributes |
150 available in the current theory context. |
150 available in the current theory context. |
151 |
151 |
152 \item [@{command "print_theorems"}] prints theorems resulting from |
152 \item @{command "print_theorems"} prints theorems resulting from |
153 the last command. |
153 the last command. |
154 |
154 |
155 \item [@{command "find_theorems"}~@{text criteria}] retrieves facts |
155 \item @{command "find_theorems"}~@{text criteria} retrieves facts |
156 from the theory or proof context matching all of given search |
156 from the theory or proof context matching all of given search |
157 criteria. The criterion @{text "name: p"} selects all theorems |
157 criteria. The criterion @{text "name: p"} selects all theorems |
158 whose fully qualified name matches pattern @{text p}, which may |
158 whose fully qualified name matches pattern @{text p}, which may |
159 contain ``@{text "*"}'' wildcards. The criteria @{text intro}, |
159 contain ``@{text "*"}'' wildcards. The criteria @{text intro}, |
160 @{text elim}, and @{text dest} select theorems that match the |
160 @{text elim}, and @{text dest} select theorems that match the |
170 yields \emph{all} currently known facts. An optional limit for the |
170 yields \emph{all} currently known facts. An optional limit for the |
171 number of printed facts may be given; the default is 40. By |
171 number of printed facts may be given; the default is 40. By |
172 default, duplicates are removed from the search result. Use |
172 default, duplicates are removed from the search result. Use |
173 @{text with_dups} to display duplicates. |
173 @{text with_dups} to display duplicates. |
174 |
174 |
175 \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] |
175 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
176 visualizes dependencies of facts, using Isabelle's graph browser |
176 visualizes dependencies of facts, using Isabelle's graph browser |
177 tool (see also \cite{isabelle-sys}). |
177 tool (see also \cite{isabelle-sys}). |
178 |
178 |
179 \item [@{command "print_facts"}] prints all local facts of the |
179 \item @{command "print_facts"} prints all local facts of the |
180 current context, both named and unnamed ones. |
180 current context, both named and unnamed ones. |
181 |
181 |
182 \item [@{command "print_binds"}] prints all term abbreviations |
182 \item @{command "print_binds"} prints all term abbreviations |
183 present in the context. |
183 present in the context. |
184 |
184 |
185 \end{descr} |
185 \end{description} |
186 *} |
186 *} |
187 |
187 |
188 |
188 |
189 section {* History commands \label{sec:history} *} |
189 section {* History commands \label{sec:history} *} |
190 |
190 |