7 chapter {* Other commands \label{ch:pure-syntax} *}
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_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
16 @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
17 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
18 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
19 @{command_def "find_theorems"}@{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')? ')')?) (criterion *)
31 criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
32 'simp' ':' term | term)
38 These commands print certain parts of the theory and proof context.
39 Note that there are some further ones available, such as for the set
40 of rules declared for simplifications.
44 \item @{command "print_commands"} prints Isabelle's outer theory
45 syntax, including keywords and command.
47 \item @{command "print_theory"} prints the main logical content of
48 the theory context; the ``@{text "!"}'' option indicates extra
51 \item @{command "print_syntax"} prints the inner syntax of types and
52 terms, depending on the current context. The output can be very
53 verbose, including grammar tables and syntax translation rules. See
54 \chref{ch:inner-syntax} for further information on inner syntax.
56 \item @{command "print_methods"} prints all proof methods
57 available in the current theory context.
59 \item @{command "print_attributes"} prints all attributes
60 available in the current theory context.
62 \item @{command "print_theorems"} prints theorems resulting from
65 \item @{command "find_theorems"}~@{text criteria} retrieves facts
66 from the theory or proof context matching all of given search
67 criteria. The criterion @{text "name: p"} selects all theorems
68 whose fully qualified name matches pattern @{text p}, which may
69 contain ``@{text "*"}'' wildcards. The criteria @{text intro},
70 @{text elim}, and @{text dest} select theorems that match the
71 current goal as introduction, elimination or destruction rules,
72 respectively. The criterion @{text "simp: t"} selects all rewrite
73 rules whose left-hand side matches the given term. The criterion
74 term @{text t} selects all theorems that contain the pattern @{text
75 t} -- as usual, patterns may contain occurrences of the dummy
76 ``@{text _}'', schematic variables, and type constraints.
78 Criteria can be preceded by ``@{text "-"}'' to select theorems that
79 do \emph{not} match. Note that giving the empty list of criteria
80 yields \emph{all} currently known facts. An optional limit for the
81 number of printed facts may be given; the default is 40. By
82 default, duplicates are removed from the search result. Use
83 @{text with_dups} to display duplicates.
85 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
86 visualizes dependencies of facts, using Isabelle's graph browser
87 tool (see also \cite{isabelle-sys}).
89 \item @{command "print_facts"} prints all local facts of the
90 current context, both named and unnamed ones.
92 \item @{command "print_binds"} prints all term abbreviations
93 present in the context.
99 section {* History commands \label{sec:history} *}
102 \begin{matharray}{rcl}
103 @{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
104 @{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
105 @{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
108 The Isabelle/Isar top-level maintains a two-stage history, for
109 theory and proof state transformation. Basically, any command can
110 be undone using @{command "undo"}, excluding mere diagnostic
111 elements. Note that a theorem statement with a \emph{finished}
112 proof is treated as a single unit by @{command "undo"}. In
113 contrast, the variant @{command "linear_undo"} admits to step back
114 into the middle of a proof. The @{command "kill"} command aborts
115 the current history node altogether, discontinuing a proof or even
116 the whole theory. This operation is \emph{not} undo-able.
119 History commands should never be used with user interfaces such as
120 Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
121 care of stepping forth and back itself. Interfering by manual
122 @{command "undo"}, @{command "linear_undo"}, or even @{command
123 "kill"} commands would quickly result in utter confusion.
128 section {* System commands *}
131 \begin{matharray}{rcl}
132 @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
133 @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
134 @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
138 ('cd' | 'use\_thy' | 'update\_thy') name
144 \item @{command "cd"}~@{text path} changes the current directory
145 of the Isabelle process.
147 \item @{command "pwd"} prints the current working directory.
149 \item @{command "use_thy"}~@{text A} preload theory @{text A}.
150 These system commands are scarcely used when working interactively,
151 since loading of theories is done automatically as required.