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
52 and terms, depending on the current context. The output can be very
53 verbose, including grammar tables and syntax translation rules. See
54 \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
57 \item @{command "print_methods"} prints all proof methods
58 available in the current theory context.
60 \item @{command "print_attributes"} prints all attributes
61 available in the current theory context.
63 \item @{command "print_theorems"} prints theorems resulting from
66 \item @{command "find_theorems"}~@{text criteria} retrieves facts
67 from the theory or proof context matching all of given search
68 criteria. The criterion @{text "name: p"} selects all theorems
69 whose fully qualified name matches pattern @{text p}, which may
70 contain ``@{text "*"}'' wildcards. The criteria @{text intro},
71 @{text elim}, and @{text dest} select theorems that match the
72 current goal as introduction, elimination or destruction rules,
73 respectively. The criterion @{text "simp: t"} selects all rewrite
74 rules whose left-hand side matches the given term. The criterion
75 term @{text t} selects all theorems that contain the pattern @{text
76 t} -- as usual, patterns may contain occurrences of the dummy
77 ``@{text _}'', schematic 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 "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
87 visualizes dependencies of facts, using Isabelle's graph browser
88 tool (see also \cite{isabelle-sys}).
90 \item @{command "print_facts"} prints all local facts of the
91 current context, both named and unnamed ones.
93 \item @{command "print_binds"} prints all term abbreviations
94 present in the context.
100 section {* History commands \label{sec:history} *}
103 \begin{matharray}{rcl}
104 @{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
105 @{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
106 @{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
109 The Isabelle/Isar top-level maintains a two-stage history, for
110 theory and proof state transformation. Basically, any command can
111 be undone using @{command "undo"}, excluding mere diagnostic
112 elements. Note that a theorem statement with a \emph{finished}
113 proof is treated as a single unit by @{command "undo"}. In
114 contrast, the variant @{command "linear_undo"} admits to step back
115 into the middle of a proof. The @{command "kill"} command aborts
116 the current history node altogether, discontinuing a proof or even
117 the whole theory. This operation is \emph{not} undo-able.
120 History commands should never be used with user interfaces such as
121 Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
122 care of stepping forth and back itself. Interfering by manual
123 @{command "undo"}, @{command "linear_undo"}, or even @{command
124 "kill"} commands would quickly result in utter confusion.
129 section {* System commands *}
132 \begin{matharray}{rcl}
133 @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
134 @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
135 @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
139 ('cd' | 'use\_thy' | 'update\_thy') name
145 \item @{command "cd"}~@{text path} changes the current directory
146 of the Isabelle process.
148 \item @{command "pwd"} prints the current working directory.
150 \item @{command "use_thy"}~@{text A} preload theory @{text A}.
151 These system commands are scarcely used when working interactively,
152 since loading of theories is done automatically as required.