wenzelm@27052
|
1 |
%
|
wenzelm@27052
|
2 |
\begin{isabellebody}%
|
wenzelm@27052
|
3 |
\def\isabellecontext{Misc}%
|
wenzelm@27052
|
4 |
%
|
wenzelm@27052
|
5 |
\isadelimtheory
|
wenzelm@27052
|
6 |
%
|
wenzelm@27052
|
7 |
\endisadelimtheory
|
wenzelm@27052
|
8 |
%
|
wenzelm@27052
|
9 |
\isatagtheory
|
wenzelm@27052
|
10 |
\isacommand{theory}\isamarkupfalse%
|
wenzelm@27052
|
11 |
\ Misc\isanewline
|
wenzelm@43522
|
12 |
\isakeyword{imports}\ Base\ Main\isanewline
|
wenzelm@27052
|
13 |
\isakeyword{begin}%
|
wenzelm@27052
|
14 |
\endisatagtheory
|
wenzelm@27052
|
15 |
{\isafoldtheory}%
|
wenzelm@27052
|
16 |
%
|
wenzelm@27052
|
17 |
\isadelimtheory
|
wenzelm@27052
|
18 |
%
|
wenzelm@27052
|
19 |
\endisadelimtheory
|
wenzelm@27052
|
20 |
%
|
wenzelm@28788
|
21 |
\isamarkupchapter{Other commands%
|
wenzelm@27052
|
22 |
}
|
wenzelm@27052
|
23 |
\isamarkuptrue%
|
wenzelm@27052
|
24 |
%
|
wenzelm@27052
|
25 |
\isamarkupsection{Inspecting the context%
|
wenzelm@27052
|
26 |
}
|
wenzelm@27052
|
27 |
\isamarkuptrue%
|
wenzelm@27052
|
28 |
%
|
wenzelm@27052
|
29 |
\begin{isamarkuptext}%
|
wenzelm@27052
|
30 |
\begin{matharray}{rcl}
|
wenzelm@40685
|
31 |
\indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}commands}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
32 |
\indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
33 |
\indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}methods}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
34 |
\indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}attributes}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
35 |
\indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
36 |
\indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
37 |
\indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
38 |
\indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
berghofe@41872
|
39 |
\indexdef{}{command}{unused\_thms}\hypertarget{command.unused-thms}{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
40 |
\indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
41 |
\indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@27052
|
42 |
\end{matharray}
|
wenzelm@27052
|
43 |
|
wenzelm@43467
|
44 |
\begin{railoutput}
|
wenzelm@43535
|
45 |
\rail@begin{2}{}
|
wenzelm@43467
|
46 |
\rail@bar
|
wenzelm@43467
|
47 |
\rail@term{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}[]
|
wenzelm@43467
|
48 |
\rail@nextbar{1}
|
wenzelm@43467
|
49 |
\rail@term{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]
|
wenzelm@43467
|
50 |
\rail@endbar
|
wenzelm@43467
|
51 |
\rail@bar
|
wenzelm@43467
|
52 |
\rail@nextbar{1}
|
wenzelm@43467
|
53 |
\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
|
wenzelm@43467
|
54 |
\rail@endbar
|
wenzelm@43467
|
55 |
\rail@end
|
wenzelm@43535
|
56 |
\rail@begin{6}{}
|
wenzelm@43467
|
57 |
\rail@term{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]
|
wenzelm@43467
|
58 |
\rail@bar
|
wenzelm@43467
|
59 |
\rail@nextbar{1}
|
wenzelm@43467
|
60 |
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
|
wenzelm@43467
|
61 |
\rail@bar
|
wenzelm@43467
|
62 |
\rail@nextbar{2}
|
wenzelm@43467
|
63 |
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
|
wenzelm@43467
|
64 |
\rail@endbar
|
wenzelm@43467
|
65 |
\rail@bar
|
wenzelm@43467
|
66 |
\rail@nextbar{2}
|
wenzelm@43467
|
67 |
\rail@term{\isa{with{\isaliteral{5F}{\isacharunderscore}}dups}}[]
|
wenzelm@43467
|
68 |
\rail@endbar
|
wenzelm@43467
|
69 |
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
|
wenzelm@43467
|
70 |
\rail@endbar
|
wenzelm@43467
|
71 |
\rail@cr{4}
|
wenzelm@43467
|
72 |
\rail@plus
|
wenzelm@43467
|
73 |
\rail@nextplus{5}
|
wenzelm@43467
|
74 |
\rail@cnont{\isa{thmcriterion}}[]
|
wenzelm@43467
|
75 |
\rail@endplus
|
wenzelm@43467
|
76 |
\rail@end
|
wenzelm@43467
|
77 |
\rail@begin{7}{\isa{thmcriterion}}
|
wenzelm@43467
|
78 |
\rail@bar
|
wenzelm@43467
|
79 |
\rail@nextbar{1}
|
wenzelm@43467
|
80 |
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
|
wenzelm@43467
|
81 |
\rail@endbar
|
wenzelm@43467
|
82 |
\rail@bar
|
wenzelm@43467
|
83 |
\rail@term{\isa{name}}[]
|
wenzelm@43467
|
84 |
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
|
wenzelm@43467
|
85 |
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
|
wenzelm@43467
|
86 |
\rail@nextbar{1}
|
wenzelm@43467
|
87 |
\rail@term{\isa{intro}}[]
|
wenzelm@43467
|
88 |
\rail@nextbar{2}
|
wenzelm@43467
|
89 |
\rail@term{\isa{elim}}[]
|
wenzelm@43467
|
90 |
\rail@nextbar{3}
|
wenzelm@43467
|
91 |
\rail@term{\isa{dest}}[]
|
wenzelm@43467
|
92 |
\rail@nextbar{4}
|
wenzelm@43467
|
93 |
\rail@term{\isa{solves}}[]
|
wenzelm@43467
|
94 |
\rail@nextbar{5}
|
wenzelm@43467
|
95 |
\rail@term{\isa{simp}}[]
|
wenzelm@43467
|
96 |
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
|
wenzelm@43467
|
97 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
|
wenzelm@43467
|
98 |
\rail@nextbar{6}
|
wenzelm@43467
|
99 |
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
|
wenzelm@43467
|
100 |
\rail@endbar
|
wenzelm@43467
|
101 |
\rail@end
|
wenzelm@43535
|
102 |
\rail@begin{2}{}
|
wenzelm@43467
|
103 |
\rail@term{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}[]
|
wenzelm@43467
|
104 |
\rail@plus
|
wenzelm@43467
|
105 |
\rail@nextplus{1}
|
wenzelm@43467
|
106 |
\rail@cnont{\isa{constcriterion}}[]
|
wenzelm@43467
|
107 |
\rail@endplus
|
wenzelm@43467
|
108 |
\rail@end
|
wenzelm@43467
|
109 |
\rail@begin{3}{\isa{constcriterion}}
|
wenzelm@43467
|
110 |
\rail@bar
|
wenzelm@43467
|
111 |
\rail@nextbar{1}
|
wenzelm@43467
|
112 |
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
|
wenzelm@43467
|
113 |
\rail@endbar
|
wenzelm@43467
|
114 |
\rail@bar
|
wenzelm@43467
|
115 |
\rail@term{\isa{name}}[]
|
wenzelm@43467
|
116 |
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
|
wenzelm@43467
|
117 |
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
|
wenzelm@43467
|
118 |
\rail@nextbar{1}
|
wenzelm@43467
|
119 |
\rail@term{\isa{strict}}[]
|
wenzelm@43467
|
120 |
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
|
wenzelm@43467
|
121 |
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
|
wenzelm@43467
|
122 |
\rail@nextbar{2}
|
wenzelm@43467
|
123 |
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
|
wenzelm@43467
|
124 |
\rail@endbar
|
wenzelm@43467
|
125 |
\rail@end
|
wenzelm@43535
|
126 |
\rail@begin{1}{}
|
wenzelm@43467
|
127 |
\rail@term{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
|
wenzelm@43467
|
128 |
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
|
wenzelm@43467
|
129 |
\rail@end
|
wenzelm@43535
|
130 |
\rail@begin{3}{}
|
wenzelm@43467
|
131 |
\rail@term{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
|
wenzelm@43467
|
132 |
\rail@bar
|
wenzelm@43467
|
133 |
\rail@nextbar{1}
|
wenzelm@43467
|
134 |
\rail@plus
|
wenzelm@43467
|
135 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
wenzelm@43467
|
136 |
\rail@nextplus{2}
|
wenzelm@43467
|
137 |
\rail@endplus
|
wenzelm@43467
|
138 |
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
|
wenzelm@43467
|
139 |
\rail@plus
|
wenzelm@43467
|
140 |
\rail@nextplus{2}
|
wenzelm@43467
|
141 |
\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
wenzelm@43467
|
142 |
\rail@endplus
|
wenzelm@43467
|
143 |
\rail@endbar
|
wenzelm@43467
|
144 |
\rail@end
|
wenzelm@43467
|
145 |
\end{railoutput}
|
wenzelm@27052
|
146 |
|
wenzelm@27052
|
147 |
|
wenzelm@27052
|
148 |
These commands print certain parts of the theory and proof context.
|
wenzelm@27052
|
149 |
Note that there are some further ones available, such as for the set
|
wenzelm@27052
|
150 |
of rules declared for simplifications.
|
wenzelm@27052
|
151 |
|
wenzelm@28788
|
152 |
\begin{description}
|
wenzelm@27052
|
153 |
|
wenzelm@40685
|
154 |
\item \hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}commands}}}} prints Isabelle's outer theory
|
wenzelm@27052
|
155 |
syntax, including keywords and command.
|
wenzelm@27052
|
156 |
|
wenzelm@40685
|
157 |
\item \hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}} prints the main logical content of
|
wenzelm@40685
|
158 |
the theory context; the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' option indicates extra
|
wenzelm@27052
|
159 |
verbosity.
|
wenzelm@27052
|
160 |
|
wenzelm@40685
|
161 |
\item \hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}methods}}}} prints all proof methods
|
wenzelm@27052
|
162 |
available in the current theory context.
|
wenzelm@27052
|
163 |
|
wenzelm@40685
|
164 |
\item \hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}attributes}}}} prints all attributes
|
wenzelm@27052
|
165 |
available in the current theory context.
|
wenzelm@27052
|
166 |
|
wenzelm@40685
|
167 |
\item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}} prints theorems resulting from the
|
wenzelm@40685
|
168 |
last command; the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' option indicates extra verbosity.
|
wenzelm@27052
|
169 |
|
wenzelm@40685
|
170 |
\item \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}~\isa{criteria} retrieves facts
|
wenzelm@27052
|
171 |
from the theory or proof context matching all of given search
|
wenzelm@40685
|
172 |
criteria. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ p{\isaliteral{22}{\isachardoublequote}}} selects all theorems
|
wenzelm@27052
|
173 |
whose fully qualified name matches pattern \isa{p}, which may
|
wenzelm@40685
|
174 |
contain ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' wildcards. The criteria \isa{intro},
|
wenzelm@27052
|
175 |
\isa{elim}, and \isa{dest} select theorems that match the
|
wenzelm@27052
|
176 |
current goal as introduction, elimination or destruction rules,
|
wenzelm@40685
|
177 |
respectively. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}solves{\isaliteral{22}{\isachardoublequote}}} returns all rules
|
kleing@29830
|
178 |
that would directly solve the current goal. The criterion
|
wenzelm@40685
|
179 |
\isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}\ t{\isaliteral{22}{\isachardoublequote}}} selects all rewrite rules whose left-hand side
|
kleing@29830
|
180 |
matches the given term. The criterion term \isa{t} selects all
|
kleing@29830
|
181 |
theorems that contain the pattern \isa{t} -- as usual, patterns
|
wenzelm@40685
|
182 |
may contain occurrences of the dummy ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'', schematic
|
kleing@29830
|
183 |
variables, and type constraints.
|
wenzelm@27052
|
184 |
|
wenzelm@40685
|
185 |
Criteria can be preceded by ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' to select theorems that
|
wenzelm@27052
|
186 |
do \emph{not} match. Note that giving the empty list of criteria
|
wenzelm@27052
|
187 |
yields \emph{all} currently known facts. An optional limit for the
|
wenzelm@27052
|
188 |
number of printed facts may be given; the default is 40. By
|
wenzelm@27052
|
189 |
default, duplicates are removed from the search result. Use
|
wenzelm@40685
|
190 |
\isa{with{\isaliteral{5F}{\isacharunderscore}}dups} to display duplicates.
|
kleing@29831
|
191 |
|
wenzelm@40685
|
192 |
\item \hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}~\isa{criteria} prints all constants
|
wenzelm@40685
|
193 |
whose type meets all of the given criteria. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}strict{\isaliteral{3A}{\isacharcolon}}\ ty{\isaliteral{22}{\isachardoublequote}}} is met by any type that matches the type pattern
|
wenzelm@40685
|
194 |
\isa{ty}. Patterns may contain both the dummy type ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''
|
kleing@29831
|
195 |
and sort constraints. The criterion \isa{ty} is similar, but it
|
wenzelm@40685
|
196 |
also matches against subtypes. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ p{\isaliteral{22}{\isachardoublequote}}} and
|
wenzelm@40685
|
197 |
the prefix ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' function as described for \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}.
|
kleing@29831
|
198 |
|
wenzelm@40685
|
199 |
\item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
|
wenzelm@27052
|
200 |
visualizes dependencies of facts, using Isabelle's graph browser
|
wenzelm@27052
|
201 |
tool (see also \cite{isabelle-sys}).
|
berghofe@41872
|
202 |
|
berghofe@41872
|
203 |
\item \hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m\ {\isaliteral{2D}{\isacharminus}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}
|
berghofe@41872
|
204 |
displays all unused theorems in theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}
|
berghofe@41872
|
205 |
or their parents, but not in \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{22}{\isachardoublequote}}} or their parents.
|
berghofe@41872
|
206 |
If \isa{n} is \isa{{\isadigit{0}}}, the end of the range of theories
|
berghofe@41872
|
207 |
defaults to the current theory. If no range is specified,
|
berghofe@41872
|
208 |
only the unused theorems in the current theory are displayed.
|
wenzelm@27052
|
209 |
|
wenzelm@40685
|
210 |
\item \hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}} prints all local facts of the
|
wenzelm@27052
|
211 |
current context, both named and unnamed ones.
|
wenzelm@27052
|
212 |
|
wenzelm@40685
|
213 |
\item \hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}} prints all term abbreviations
|
wenzelm@27052
|
214 |
present in the context.
|
wenzelm@27052
|
215 |
|
wenzelm@28788
|
216 |
\end{description}%
|
wenzelm@27052
|
217 |
\end{isamarkuptext}%
|
wenzelm@27052
|
218 |
\isamarkuptrue%
|
wenzelm@27052
|
219 |
%
|
wenzelm@27054
|
220 |
\isamarkupsection{System commands%
|
wenzelm@27052
|
221 |
}
|
wenzelm@27052
|
222 |
\isamarkuptrue%
|
wenzelm@27052
|
223 |
%
|
wenzelm@27052
|
224 |
\begin{isamarkuptext}%
|
wenzelm@27052
|
225 |
\begin{matharray}{rcl}
|
wenzelm@40685
|
226 |
\indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
227 |
\indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@40685
|
228 |
\indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
|
wenzelm@27052
|
229 |
\end{matharray}
|
wenzelm@27052
|
230 |
|
wenzelm@43467
|
231 |
\begin{railoutput}
|
wenzelm@43535
|
232 |
\rail@begin{2}{}
|
wenzelm@43467
|
233 |
\rail@bar
|
wenzelm@43467
|
234 |
\rail@term{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}[]
|
wenzelm@43467
|
235 |
\rail@nextbar{1}
|
wenzelm@43467
|
236 |
\rail@term{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}}[]
|
wenzelm@43467
|
237 |
\rail@endbar
|
wenzelm@43467
|
238 |
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
|
wenzelm@43467
|
239 |
\rail@end
|
wenzelm@43467
|
240 |
\end{railoutput}
|
wenzelm@43467
|
241 |
|
wenzelm@27052
|
242 |
|
wenzelm@28788
|
243 |
\begin{description}
|
wenzelm@27052
|
244 |
|
wenzelm@28788
|
245 |
\item \hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path} changes the current directory
|
wenzelm@27052
|
246 |
of the Isabelle process.
|
wenzelm@27052
|
247 |
|
wenzelm@28788
|
248 |
\item \hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}} prints the current working directory.
|
wenzelm@27052
|
249 |
|
wenzelm@40685
|
250 |
\item \hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}~\isa{A} preload theory \isa{A}.
|
wenzelm@27052
|
251 |
These system commands are scarcely used when working interactively,
|
wenzelm@27052
|
252 |
since loading of theories is done automatically as required.
|
wenzelm@27052
|
253 |
|
wenzelm@40275
|
254 |
\end{description}
|
wenzelm@40275
|
255 |
|
wenzelm@40275
|
256 |
%FIXME proper place (!?)
|
wenzelm@40275
|
257 |
Isabelle file specification may contain path variables (e.g.\
|
wenzelm@40275
|
258 |
\verb|$ISABELLE_HOME|) that are expanded accordingly. Note
|
wenzelm@48538
|
259 |
that \verb|~| abbreviates \verb|$USER_HOME|, and
|
wenzelm@48538
|
260 |
\verb|~~| abbreviates \verb|$ISABELLE_HOME|. The
|
wenzelm@48538
|
261 |
general syntax for path specifications follows POSIX conventions.%
|
wenzelm@27052
|
262 |
\end{isamarkuptext}%
|
wenzelm@27052
|
263 |
\isamarkuptrue%
|
wenzelm@27052
|
264 |
%
|
wenzelm@27052
|
265 |
\isadelimtheory
|
wenzelm@27052
|
266 |
%
|
wenzelm@27052
|
267 |
\endisadelimtheory
|
wenzelm@27052
|
268 |
%
|
wenzelm@27052
|
269 |
\isatagtheory
|
wenzelm@27052
|
270 |
\isacommand{end}\isamarkupfalse%
|
wenzelm@27052
|
271 |
%
|
wenzelm@27052
|
272 |
\endisatagtheory
|
wenzelm@27052
|
273 |
{\isafoldtheory}%
|
wenzelm@27052
|
274 |
%
|
wenzelm@27052
|
275 |
\isadelimtheory
|
wenzelm@27052
|
276 |
%
|
wenzelm@27052
|
277 |
\endisadelimtheory
|
wenzelm@27052
|
278 |
\isanewline
|
wenzelm@27052
|
279 |
\end{isabellebody}%
|
wenzelm@27052
|
280 |
%%% Local Variables:
|
wenzelm@27052
|
281 |
%%% mode: latex
|
wenzelm@27052
|
282 |
%%% TeX-master: "root"
|
wenzelm@27052
|
283 |
%%% End:
|