author | wenzelm |
Thu, 31 Aug 2006 14:53:55 +0200 | |
changeset 20447 | 5b75f1c4d7d6 |
parent 20064 | 92aad017b847 |
child 20451 | 27ea2ba48fa3 |
permissions | -rw-r--r-- |
18537 | 1 |
|
2 |
(* $Id$ *) |
|
3 |
||
4 |
theory integration imports base begin |
|
5 |
||
6 |
chapter {* System integration *} |
|
7 |
||
20447 | 8 |
section {* Isar toplevel \label{sec:isar-toplevel} *} |
18537 | 9 |
|
10 |
text {* The Isar toplevel may be considered the centeral hub of the |
|
11 |
Isabelle/Isar system, where all key components and sub-systems are |
|
12 |
integrated into a single read-eval-print loop of Isar commands. |
|
13 |
Here we even incorporate the existing {\ML} toplevel of the compiler |
|
14 |
and run-time system (cf.\ \secref{sec:ML-toplevel}). |
|
15 |
||
16 |
Isabelle/Isar departs from original ``LCF system architecture'' |
|
17 |
where {\ML} was really The Meta Language for defining theories and |
|
18 |
conducting proofs. Instead, {\ML} merely serves as the |
|
19 |
implementation language for the system (and user extensions), while |
|
20 |
our specific Isar toplevel supports particular notions of |
|
21 |
incremental theory and proof development more directly. This |
|
22 |
includes the graph structure of theories and the block structure of |
|
23 |
proofs, support for unlimited undo, facilities for tracing, |
|
24 |
debugging, timing, profiling. |
|
25 |
||
26 |
\medskip The toplevel maintains an implicit state, which is |
|
27 |
transformed by a sequence of transitions -- either interactively or |
|
28 |
in batch-mode. In interactive mode, Isar state transitions are |
|
29 |
encapsulated as safe transactions, such that both failure and undo |
|
30 |
are handled conveniently without destroying the underlying draft |
|
31 |
theory (cf.~\secref{sec:context-theory}). In batch mode, |
|
32 |
transitions operate in a strictly linear (destructive) fashion, such |
|
33 |
that error conditions abort the present attempt to construct a |
|
34 |
theory altogether. |
|
35 |
||
36 |
The toplevel state is a disjoint sum of empty @{text toplevel}, or |
|
37 |
@{text theory}, or @{text proof}. On entering the main Isar loop we |
|
38 |
start with an empty toplevel. A theory is commenced by giving a |
|
39 |
@{text \<THEORY>} header; within a theory we may issue theory |
|
20025 | 40 |
commands such as @{text \<DEFINITION>}, or state a @{text |
41 |
\<THEOREM>} to be proven. Now we are within a proof state, with a |
|
42 |
rich collection of Isar proof commands for structured proof |
|
18537 | 43 |
composition, or unstructured proof scripts. When the proof is |
44 |
concluded we get back to the theory, which is then updated by |
|
45 |
storing the resulting fact. Further theory declarations or theorem |
|
46 |
statements with proofs may follow, until we eventually conclude the |
|
47 |
theory development by issuing @{text \<END>}. The resulting theory |
|
48 |
is then stored within the theory database and we are back to the |
|
49 |
empty toplevel. |
|
50 |
||
51 |
In addition to these proper state transformations, there are also |
|
52 |
some diagnostic commands for peeking at the toplevel state without |
|
53 |
modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term}, |
|
54 |
\isakeyword{print-cases}). |
|
55 |
*} |
|
56 |
||
57 |
text %mlref {* |
|
58 |
\begin{mldecls} |
|
59 |
@{index_ML_type Toplevel.state} \\ |
|
60 |
@{index_ML Toplevel.UNDEF: "exn"} \\ |
|
61 |
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ |
|
62 |
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ |
|
63 |
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ |
|
64 |
@{index_ML Toplevel.debug: "bool ref"} \\ |
|
65 |
@{index_ML Toplevel.timing: "bool ref"} \\ |
|
66 |
@{index_ML Toplevel.profiling: "int ref"} \\ |
|
67 |
\end{mldecls} |
|
68 |
||
69 |
\begin{description} |
|
70 |
||
71 |
\item @{ML_type Toplevel.state} represents Isar toplevel states, |
|
72 |
which are normally only manipulated through the toplevel transition |
|
73 |
concept (\secref{sec:toplevel-transition}). Also note that a |
|
74 |
toplevel state is subject to the same linerarity restrictions as a |
|
75 |
theory context (cf.~\secref{sec:context-theory}). |
|
76 |
||
77 |
\item @{ML Toplevel.UNDEF} is raised for undefined toplevel |
|
78 |
operations: @{ML_type Toplevel.state} is a sum type, many operations |
|
79 |
work only partially for certain cases. |
|
80 |
||
81 |
\item @{ML Toplevel.is_toplevel} checks for an empty toplevel state. |
|
82 |
||
83 |
\item @{ML Toplevel.theory_of} gets the theory of a theory or proof |
|
84 |
(!), otherwise raises @{ML Toplevel.UNDEF}. |
|
85 |
||
86 |
\item @{ML Toplevel.proof_of} gets the Isar proof state if |
|
87 |
available, otherwise raises @{ML Toplevel.UNDEF}. |
|
88 |
||
89 |
\item @{ML "set Toplevel.debug"} makes the toplevel print further |
|
90 |
details about internal error conditions, exceptions being raised |
|
91 |
etc. |
|
92 |
||
93 |
\item @{ML "set Toplevel.timing"} makes the toplevel print timing |
|
94 |
information for each Isar command being executed. |
|
95 |
||
96 |
\item @{ML Toplevel.profiling} controls low-level profiling of the |
|
97 |
underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time |
|
98 |
and 2 space profiling.} |
|
99 |
||
100 |
\end{description} |
|
101 |
*} |
|
102 |
||
103 |
||
104 |
subsection {* Toplevel transitions *} |
|
105 |
||
106 |
text {* An Isar toplevel transition consists of a partial |
|
107 |
function on the toplevel state, with additional information for |
|
108 |
diagnostics and error reporting: there are fields for command name, |
|
109 |
source position, optional source text, as well as flags for |
|
110 |
interactive-only commands (which issue a warning in batch-mode), |
|
111 |
printing of result state, etc. |
|
112 |
||
113 |
The operational part is represented as a sequential union of a list |
|
114 |
of partial functions, which are tried in turn until the first one |
|
115 |
succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}). For example, |
|
116 |
a single Isar command like \isacommand{qed} consists of the union of |
|
117 |
some function @{ML_type "Proof.state -> Proof.state"} for proofs |
|
118 |
within proofs, plus @{ML_type "Proof.state -> theory"} for proofs at |
|
119 |
the outer theory level. |
|
120 |
||
121 |
Toplevel transitions are composed via transition transformers. |
|
122 |
Internally, Isar commands are put together from an empty transition |
|
123 |
extended by name and source position (and optional source text). It |
|
124 |
is then left to the individual command parser to turn the given |
|
125 |
syntax body into a suitable transition transformer that adjoin |
|
126 |
actual operations on a theory or proof state etc. |
|
127 |
*} |
|
128 |
||
129 |
text %mlref {* |
|
130 |
\begin{mldecls} |
|
131 |
@{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\ |
|
132 |
@{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\ |
|
133 |
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) -> |
|
134 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
135 |
@{index_ML Toplevel.theory: "(theory -> theory) -> |
|
136 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
137 |
@{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> |
|
138 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
139 |
@{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> |
|
140 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
141 |
@{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) -> |
|
142 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
143 |
@{index_ML Toplevel.proof_to_theory: "(Proof.state -> theory) -> |
|
144 |
Toplevel.transition -> Toplevel.transition"} \\ |
|
145 |
\end{mldecls} |
|
146 |
||
147 |
\begin{description} |
|
148 |
||
149 |
\item @{ML Toplevel.print} sets the print flag, which causes the |
|
150 |
resulting state of the transition to be echoed in interactive mode. |
|
151 |
||
152 |
\item @{ML Toplevel.no_timing} indicates that the transition should |
|
153 |
never show timing information, e.g.\ because it is merely a |
|
154 |
diagnostic command. |
|
155 |
||
156 |
\item @{ML Toplevel.keep} adjoins a diagnostic function. |
|
157 |
||
158 |
\item @{ML Toplevel.theory} adjoins a theory transformer. |
|
159 |
||
160 |
\item @{ML Toplevel.theory_to_proof} adjoins a global goal function, |
|
18590
f6a553aa3d81
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents:
18563
diff
changeset
|
161 |
which turns a theory into a proof state. The theory may be changed |
f6a553aa3d81
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents:
18563
diff
changeset
|
162 |
before entering the proof; the generic Isar goal setup includes an |
f6a553aa3d81
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents:
18563
diff
changeset
|
163 |
argument that specifies how to apply the proven result to the |
f6a553aa3d81
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
wenzelm
parents:
18563
diff
changeset
|
164 |
theory, when the proof is finished. |
18558 | 165 |
|
18537 | 166 |
\item @{ML Toplevel.proof} adjoins a deterministic proof command, |
167 |
with a singleton result state. |
|
168 |
||
169 |
\item @{ML Toplevel.proofs} adjoins a general proof command, with |
|
170 |
zero or more result states (represented as a lazy list). |
|
171 |
||
172 |
\item @{ML Toplevel.proof_to_theory} adjoins a concluding proof |
|
173 |
command, that returns the resulting theory, after storing the |
|
174 |
resulting facts etc. |
|
175 |
||
176 |
\end{description} |
|
177 |
*} |
|
178 |
||
179 |
||
180 |
subsection {* Toplevel control *} |
|
181 |
||
182 |
text {* Apart from regular toplevel transactions there are a few |
|
183 |
special control commands that modify the behavior the toplevel |
|
184 |
itself, and only make sense in interactive mode. Under normal |
|
185 |
circumstances, the user encounters these only implicitly as part of |
|
186 |
the protocol between the Isabelle/Isar system and a user-interface |
|
187 |
such as ProofGeneral. |
|
188 |
||
189 |
\begin{description} |
|
190 |
||
191 |
\item \isacommand{undo} follows the three-level hierarchy of empty |
|
192 |
toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the |
|
193 |
previous proof context, undo after a proof reverts to the theory |
|
194 |
before the initial goal statement, undo of a theory command reverts |
|
195 |
to the previous theory value, undo of a theory header discontinues |
|
196 |
the current theory development and removes it from the theory |
|
197 |
database (\secref{sec:theory-database}). |
|
198 |
||
199 |
\item \isacommand{kill} aborts the current level of development: |
|
200 |
kill in a proof context reverts to the theory before the initial |
|
201 |
goal statement, kill in a theory context aborts the current theory |
|
202 |
development, removing it from the database. |
|
203 |
||
204 |
\item \isacommand{exit} drops out of the Isar toplevel into the |
|
205 |
underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar |
|
206 |
toplevel state is preserved and may be continued later. |
|
207 |
||
208 |
\item \isacommand{quit} terminates the Isabelle/Isar process without |
|
209 |
saving. |
|
210 |
||
211 |
\end{description} |
|
212 |
*} |
|
213 |
||
214 |
||
215 |
section {* ML toplevel \label{sec:ML-toplevel} *} |
|
216 |
||
217 |
text {* The {\ML} toplevel provides a read-compile-eval-print loop for |
|
218 |
{\ML} values, types, structures, and functors. {\ML} declarations |
|
219 |
operate on the global system state, which consists of the compiler |
|
220 |
environment plus the values of {\ML} reference variables. There is |
|
221 |
no clean way to undo {\ML} declarations, except for reverting to a |
|
222 |
previously saved state of the whole Isabelle process. {\ML} input |
|
223 |
is either read interactively from a TTY, or from a string (usually |
|
224 |
within a theory text), or from a source file (usually associated |
|
225 |
with a theory). |
|
226 |
||
227 |
Whenever the {\ML} toplevel is active, the current Isabelle theory |
|
228 |
context is passed as an internal reference variable. Thus {\ML} |
|
229 |
code may access the theory context during compilation, it may even |
|
230 |
change the value of a theory being under construction --- following |
|
231 |
the usual linearity restrictions (cf.~\secref{sec:context-theory}). |
|
232 |
*} |
|
233 |
||
234 |
text %mlref {* |
|
235 |
\begin{mldecls} |
|
236 |
@{index_ML context: "theory -> unit"} \\ |
|
237 |
@{index_ML the_context: "unit -> theory"} \\ |
|
238 |
@{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\ |
|
239 |
\end{mldecls} |
|
240 |
||
241 |
\begin{description} |
|
242 |
||
243 |
\item @{ML context}~@{text thy} sets the {\ML} theory context to |
|
244 |
@{text thy}. This is usually performed automatically by the system, |
|
245 |
when dropping out of the interactive Isar toplevel into {\ML}, or |
|
246 |
when Isar invokes {\ML} to process code from a string or a file. |
|
247 |
||
248 |
\item @{ML "the_context ()"} refers to the theory context of the |
|
249 |
{\ML} toplevel --- at compile time! {\ML} code needs to take care |
|
250 |
to refer to @{ML "the_context ()"} correctly, recall that evaluation |
|
251 |
of a function body is delayed until actual runtime. Moreover, |
|
252 |
persistent {\ML} toplevel bindings to an unfinished theory should be |
|
253 |
avoided: code should either project out the desired information |
|
254 |
immediately, or produce an explicit @{ML_type theory_ref} (cf.\ |
|
255 |
\secref{sec:context-theory}). |
|
256 |
||
257 |
\item @{ML "Context.>>"}~@{text f} applies theory transformation |
|
258 |
@{text f} to the current theory of the {\ML} toplevel. In order to |
|
259 |
work as expected, the theory should be still under construction, and |
|
260 |
the Isar language element that invoked the {\ML} compiler in the |
|
261 |
first place shoule be ready to accept the changed theory value |
|
262 |
(e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}). |
|
263 |
Otherwise the theory may get destroyed! |
|
264 |
||
265 |
\end{description} |
|
266 |
||
267 |
It is very important to note that the above functions are really |
|
268 |
restricted to the compile time, even though the {\ML} compiler is |
|
269 |
invoked at runtime! The majority of {\ML} code uses explicit |
|
270 |
functional arguments of a theory or proof context, as required. |
|
271 |
Thus it may get run in an arbitrary context later on. |
|
272 |
||
273 |
\bigskip |
|
274 |
||
275 |
\begin{mldecls} |
|
276 |
@{index_ML Isar.main: "unit -> unit"} \\ |
|
277 |
@{index_ML Isar.loop: "unit -> unit"} \\ |
|
278 |
@{index_ML Isar.state: "unit -> Toplevel.state"} \\ |
|
20025 | 279 |
@{index_ML Isar.context: "unit -> Proof.context"} \\ |
18537 | 280 |
@{index_ML Isar.exn: "unit -> (exn * string) option"} \\ |
281 |
\end{mldecls} |
|
282 |
||
283 |
\begin{description} |
|
284 |
||
285 |
\item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML}, |
|
286 |
initializing the state to empty toplevel state. |
|
287 |
||
288 |
\item @{ML "Isar.loop ()"} continues the Isar toplevel with the |
|
289 |
current state, after dropping out of the Isar toplevel loop. |
|
290 |
||
291 |
\item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current |
|
292 |
toplevel state and optional error condition, respectively. This |
|
293 |
only works after dropping out of the Isar toplevel loop. |
|
294 |
||
20025 | 295 |
\item @{ML "Isar.context ()"} produces the proof context from @{ML |
20064 | 296 |
"Isar.state ()"}. |
20025 | 297 |
|
18537 | 298 |
\end{description} |
299 |
*} |
|
300 |
||
301 |
||
302 |
section {* Theory database *} |
|
303 |
||
304 |
text {* The theory database maintains a collection of theories, |
|
305 |
together with some administrative information about the original |
|
306 |
sources, which are held in an external store (i.e.\ a collection of |
|
307 |
directories within the regular file system of the underlying |
|
308 |
platform). |
|
309 |
||
310 |
The theory database is organized as a directed acyclic graph, with |
|
311 |
entries referenced by theory name. Although some external |
|
312 |
interfaces allow to include a directory specification, this is only |
|
313 |
a hint to the underlying theory loader mechanism: the internal |
|
314 |
theory name space is flat. |
|
315 |
||
316 |
Theory @{text A} is associated with the main theory file @{text |
|
317 |
A}\verb,.thy,, which needs to be accessible through the theory |
|
318 |
loader path. A number of optional {\ML} source files may be |
|
319 |
associated with each theory, by declaring these dependencies in the |
|
320 |
theory header as @{text \<USES>}, and loading them consecutively |
|
321 |
within the theory context. The system keeps track of incoming {\ML} |
|
322 |
sources and associates them with the current theory. The special |
|
323 |
theory {\ML} file @{text A}\verb,.ML, is loaded after a theory has |
|
324 |
been concluded, in order to support legacy proof {\ML} proof |
|
325 |
scripts. |
|
326 |
||
327 |
The basic internal actions of the theory database are @{text |
|
18554 | 328 |
"update"}, @{text "outdate"}, and @{text "remove"}: |
18537 | 329 |
|
330 |
\begin{itemize} |
|
331 |
||
332 |
\item @{text "update A"} introduces a link of @{text "A"} with a |
|
333 |
@{text "theory"} value of the same name; it asserts that the theory |
|
334 |
sources are consistent with that value. |
|
335 |
||
336 |
\item @{text "outdate A"} invalidates the link of a theory database |
|
337 |
entry to its sources, but retains the present theory value. |
|
338 |
||
339 |
\item @{text "remove A"} removes entry @{text "A"} from the theory |
|
340 |
database. |
|
341 |
||
342 |
\end{itemize} |
|
343 |
||
344 |
These actions are propagated to sub- or super-graphs of a theory |
|
345 |
entry in the usual way, in order to preserve global consistency of |
|
346 |
the state of all loaded theories with the sources of the external |
|
347 |
store. This implies causal dependencies of certain actions: @{text |
|
348 |
"update"} or @{text "outdate"} of an entry will @{text "outdate"} |
|
349 |
all descendants; @{text "remove"} will @{text "remove"} all |
|
350 |
descendants. |
|
351 |
||
352 |
\medskip There are separate user-level interfaces to operate on the |
|
353 |
theory database directly or indirectly. The primitive actions then |
|
354 |
just happen automatically while working with the system. In |
|
355 |
particular, processing a theory header @{text "\<THEORY> A |
|
356 |
\<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensure that the |
|
357 |
sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"} |
|
358 |
is up-to-date. Earlier theories are reloaded as required, with |
|
359 |
@{text update} actions proceeding in topological order according to |
|
360 |
theory dependencies. There may be also a wave of implied @{text |
|
361 |
outdate} actions for derived theory nodes until a stable situation |
|
362 |
is achieved eventually. |
|
363 |
*} |
|
364 |
||
365 |
text %mlref {* |
|
366 |
\begin{mldecls} |
|
367 |
@{index_ML theory: "string -> theory"} \\ |
|
368 |
@{index_ML use_thy: "string -> unit"} \\ |
|
369 |
@{index_ML update_thy: "string -> unit"} \\ |
|
370 |
@{index_ML use_thy_only: "string -> unit"} \\ |
|
371 |
@{index_ML update_thy_only: "string -> unit"} \\ |
|
372 |
@{index_ML touch_thy: "string -> unit"} \\ |
|
373 |
@{index_ML remove_thy: "string -> unit"} \\[1ex] |
|
374 |
@{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\ |
|
375 |
@{index_ML ThyInfo.end_theory: "theory -> theory"} \\ |
|
376 |
@{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex] |
|
377 |
@{verbatim "datatype action = Update | Outdate | Remove"} \\ |
|
378 |
@{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\ |
|
379 |
\end{mldecls} |
|
380 |
||
381 |
\begin{description} |
|
382 |
||
383 |
\item @{ML theory}~@{text A} retrieves the theory value presently |
|
384 |
associated with @{text A}. The result is not necessarily |
|
385 |
up-to-date! |
|
386 |
||
387 |
\item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent |
|
388 |
or out-of-date. It ensures that all parent theories are available |
|
389 |
as well, but does not reload them if older versions are already |
|
390 |
present. |
|
391 |
||
392 |
\item @{ML update_thy} is similar to @{ML use_thy}, but ensures that |
|
393 |
the @{text A} and all of its ancestors are fully up-to-date. |
|
394 |
||
395 |
\item @{ML use_thy_only}~@{text A} is like @{ML use_thy}~@{text A}, |
|
396 |
but refrains from loading the attached @{text A}\verb,.ML, file. |
|
397 |
This is occasionally useful in replaying legacy {\ML} proof scripts |
|
398 |
by hand. |
|
399 |
||
400 |
\item @{ML update_thy_only} is analogous to @{ML use_thy_only}, but |
|
401 |
proceeds like @{ML update_thy} for ancestors. |
|
402 |
||
403 |
\item @{ML touch_thy}~@{text A} performs @{text outdate} action on |
|
404 |
theory @{text A} and all of its descendants. |
|
405 |
||
406 |
\item @{ML remove_thy}~@{text A} removes @{text A} and all of its |
|
407 |
descendants from the theory database. |
|
408 |
||
409 |
\item @{ML ThyInfo.begin_theory} is the basic operation behind a |
|
410 |
@{text \<THEORY>} header declaration. The boolean argument |
|
411 |
indicates the strictness of treating ancestors: for @{ML true} (as |
|
412 |
in interactive mode) like @{ML update_thy}, and for @{ML false} (as |
|
413 |
in batch mode) like @{ML use_thy}. This is {\ML} functions is |
|
414 |
normally not invoked directly. |
|
415 |
||
416 |
\item @{ML ThyInfo.end_theory} concludes the loading of a theory |
|
417 |
proper; an attached theory {\ML} file may be still loaded later on. |
|
418 |
This is {\ML} functions is normally not invoked directly. |
|
419 |
||
420 |
\item @{ML ThyInfo.register_theory}~{text thy} registers an existing |
|
421 |
theory value with the theory loader database. There is no |
|
422 |
management of associated sources; this is mainly for bootstrapping. |
|
423 |
||
424 |
\item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text |
|
425 |
f} as a hook for theory database actions. The function will be |
|
426 |
invoked with the action and theory name being involved; thus derived |
|
427 |
actions may be performed in associated system components, e.g.\ |
|
428 |
maintaining the state of an editor for theory sources. |
|
429 |
||
430 |
The kind and order of actions occurring in practice depends both on |
|
431 |
user interactions and the internal process of resolving theory |
|
432 |
imports. Hooks should not rely on a particular policy here! Any |
|
433 |
exceptions raised by the hook are ignored by the theory database. |
|
434 |
||
435 |
\end{description} |
|
436 |
*} |
|
437 |
||
438 |
||
439 |
(* FIXME section {* Sessions and document preparation *} *) |
|
440 |
||
441 |
end |