7 chapter {* Other commands *}
9 section {* Inspecting the context *}
12 \begin{matharray}{rcl}
13 @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
14 @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
15 @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
16 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
17 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
18 @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
19 @{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
20 @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
21 @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
22 @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
26 'print\_theory' ( '!'?)
29 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
31 thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
32 'solves' | 'simp' ':' term | term)
34 'find\_consts' (constcriterion *)
36 constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
42 These commands print certain parts of the theory and proof context.
43 Note that there are some further ones available, such as for the set
44 of rules declared for simplifications.
48 \item @{command "print_commands"} prints Isabelle's outer theory
49 syntax, including keywords and command.
51 \item @{command "print_theory"} prints the main logical content of
52 the theory context; the ``@{text "!"}'' option indicates extra
55 \item @{command "print_methods"} prints all proof methods
56 available in the current theory context.
58 \item @{command "print_attributes"} prints all attributes
59 available in the current theory context.
61 \item @{command "print_theorems"} prints theorems resulting from
64 \item @{command "find_theorems"}~@{text criteria} retrieves facts
65 from the theory or proof context matching all of given search
66 criteria. The criterion @{text "name: p"} selects all theorems
67 whose fully qualified name matches pattern @{text p}, which may
68 contain ``@{text "*"}'' wildcards. The criteria @{text intro},
69 @{text elim}, and @{text dest} select theorems that match the
70 current goal as introduction, elimination or destruction rules,
71 respectively. The criterion @{text "solves"} returns all rules
72 that would directly solve the current goal. The criterion
73 @{text "simp: t"} selects all rewrite rules whose left-hand side
74 matches the given term. The criterion term @{text t} selects all
75 theorems that contain the pattern @{text t} -- as usual, patterns
76 may contain occurrences of the dummy ``@{text _}'', schematic
77 variables, and type constraints.
79 Criteria can be preceded by ``@{text "-"}'' to select theorems that
80 do \emph{not} match. Note that giving the empty list of criteria
81 yields \emph{all} currently known facts. An optional limit for the
82 number of printed facts may be given; the default is 40. By
83 default, duplicates are removed from the search result. Use
84 @{text with_dups} to display duplicates.
86 \item @{command "find_consts"}~@{text criteria} prints all constants
87 whose type meets all of the given criteria. The criterion @{text
88 "strict: ty"} is met by any type that matches the type pattern
89 @{text ty}. Patterns may contain both the dummy type ``@{text _}''
90 and sort constraints. The criterion @{text ty} is similar, but it
91 also matches against subtypes. The criterion @{text "name: p"} and
92 the prefix ``@{text "-"}'' function as described for @{command
95 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
96 visualizes dependencies of facts, using Isabelle's graph browser
97 tool (see also \cite{isabelle-sys}).
99 \item @{command "print_facts"} prints all local facts of the
100 current context, both named and unnamed ones.
102 \item @{command "print_binds"} prints all term abbreviations
103 present in the context.
109 section {* History commands \label{sec:history} *}
112 \begin{matharray}{rcl}
113 @{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
114 @{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
115 @{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
118 The Isabelle/Isar top-level maintains a two-stage history, for
119 theory and proof state transformation. Basically, any command can
120 be undone using @{command "undo"}, excluding mere diagnostic
121 elements. Note that a theorem statement with a \emph{finished}
122 proof is treated as a single unit by @{command "undo"}. In
123 contrast, the variant @{command "linear_undo"} admits to step back
124 into the middle of a proof. The @{command "kill"} command aborts
125 the current history node altogether, discontinuing a proof or even
126 the whole theory. This operation is \emph{not} undo-able.
129 History commands should never be used with user interfaces such as
130 Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
131 care of stepping forth and back itself. Interfering by manual
132 @{command "undo"}, @{command "linear_undo"}, or even @{command
133 "kill"} commands would quickly result in utter confusion.
138 section {* System commands *}
141 \begin{matharray}{rcl}
142 @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
143 @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
144 @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
148 ('cd' | 'use\_thy' | 'update\_thy') name
154 \item @{command "cd"}~@{text path} changes the current directory
155 of the Isabelle process.
157 \item @{command "pwd"} prints the current working directory.
159 \item @{command "use_thy"}~@{text A} preload theory @{text A}.
160 These system commands are scarcely used when working interactively,
161 since loading of theories is done automatically as required.