author | wenzelm |
Wed, 03 Sep 2008 17:47:30 +0200 | |
changeset 28110 | 9d121b171a0a |
parent 28086 | db584d1d2af4 |
child 28283 | dbe9c820e4d2 |
permissions | -rw-r--r-- |
18537 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{ML}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
\isanewline |
|
18543 | 7 |
\isanewline |
18537 | 8 |
% |
9 |
\endisadelimtheory |
|
10 |
% |
|
11 |
\isatagtheory |
|
12 |
\isacommand{theory}\isamarkupfalse% |
|
18543 | 13 |
\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}% |
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
26437 | 21 |
\isamarkupchapter{Advanced ML programming% |
18543 | 22 |
} |
23 |
\isamarkuptrue% |
|
24 |
% |
|
24089 | 25 |
\isamarkupsection{Style% |
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
18543 | 29 |
\begin{isamarkuptext}% |
26459 | 30 |
Like any style guide, also this one should not be interpreted dogmatically, but |
31 |
with care and discernment. It consists of a collection of |
|
32 |
recommendations which have been turned out useful over long years of |
|
33 |
Isabelle system development and are supposed to support writing of readable |
|
34 |
and managable code. Special cases encourage derivations, |
|
35 |
as far as you know what you are doing. |
|
36 |
\footnote{This style guide is loosely based on |
|
37 |
\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}} |
|
21148 | 38 |
|
39 |
\begin{description} |
|
40 |
||
41 |
\item[fundamental law of programming] |
|
42 |
Whenever writing code, keep in mind: A program is |
|
43 |
written once, modified ten times, and read |
|
26459 | 44 |
hundred times. So simplify its writing, |
21148 | 45 |
always keep future modifications in mind, |
21172 | 46 |
and never jeopardize readability. Every second you hesitate |
21148 | 47 |
to spend on making your code more clear you will |
48 |
have to spend ten times understanding what you have |
|
49 |
written later on. |
|
50 |
||
51 |
\item[white space matters] |
|
52 |
Treat white space in your code as if it determines |
|
53 |
the meaning of code. |
|
54 |
||
55 |
\begin{itemize} |
|
56 |
||
57 |
\item The space bar is the easiest key to find on the keyboard, |
|
24089 | 58 |
press it as often as necessary. \verb|2 + 2| is better |
59 |
than \verb|2+2|, likewise \verb|f (x, y)| is |
|
60 |
better than \verb|f(x,y)|. |
|
21148 | 61 |
|
24089 | 62 |
\item Restrict your lines to 80 characters. This will allow |
63 |
you to keep the beginning of a line in view while watching |
|
64 |
its end.\footnote{To acknowledge the lax practice of |
|
65 |
text editing these days, we tolerate as much as 100 |
|
66 |
characters per line, but anything beyond 120 is not |
|
67 |
considered proper source text.} |
|
21148 | 68 |
|
24089 | 69 |
\item Ban tabulators; they are a context-sensitive formatting |
70 |
feature and likely to confuse anyone not using your favorite |
|
71 |
editor.\footnote{Some modern programming language even |
|
72 |
forbid tabulators altogether according to the formal syntax |
|
73 |
definition.} |
|
21148 | 74 |
|
75 |
\item Get rid of trailing whitespace. Instead, do not |
|
24089 | 76 |
suppress a trailing newline at the end of your files. |
21148 | 77 |
|
78 |
\item Choose a generally accepted style of indentation, |
|
79 |
then use it systematically throughout the whole |
|
80 |
application. An indentation of two spaces is appropriate. |
|
81 |
Avoid dangling indentation. |
|
82 |
||
83 |
\end{itemize} |
|
84 |
||
85 |
\item[cut-and-paste succeeds over copy-and-paste] |
|
24089 | 86 |
\emph{Never} copy-and-paste code when programming. If you |
21148 | 87 |
need the same piece of code twice, introduce a |
88 |
reasonable auxiliary function (if there is no |
|
89 |
such function, very likely you got something wrong). |
|
90 |
Any copy-and-paste will turn out to be painful |
|
26459 | 91 |
when something has to be changed later on. |
21148 | 92 |
|
93 |
\item[comments] |
|
94 |
are a device which requires careful thinking before using |
|
95 |
it. The best comment for your code should be the code itself. |
|
96 |
Prefer efforts to write clear, understandable code |
|
97 |
over efforts to explain nasty code. |
|
98 |
||
99 |
\item[functional programming is based on functions] |
|
26459 | 100 |
Model things as abstract as appropriate. Avoid unnecessarrily |
101 |
concrete datatype representations. For example, consider a function |
|
102 |
taking some table data structure as argument and performing |
|
103 |
lookups on it. Instead of taking a table, it could likewise |
|
104 |
take just a lookup function. Accustom |
|
24089 | 105 |
your way of coding to the level of expressiveness a functional |
106 |
programming language is giving onto you. |
|
21148 | 107 |
|
108 |
\item[tuples] |
|
109 |
are often in the way. When there is no striking argument |
|
110 |
to tuple function arguments, just write your function curried. |
|
111 |
||
112 |
\item[telling names] |
|
24089 | 113 |
Any name should tell its purpose as exactly as possible, while |
114 |
keeping its length to the absolutely necessary minimum. Always |
|
115 |
give the same name to function arguments which have the same |
|
116 |
meaning. Separate words by underscores (\verb|int_of_string|, not \verb|intOfString|).\footnote{Some |
|
117 |
recent tools for Emacs include special precautions to cope with |
|
118 |
bumpy names in \isa{camelCase}, e.g.\ for improved on-screen |
|
119 |
readability. It is easier to abstain from using such names in the |
|
120 |
first place.} |
|
21148 | 121 |
|
122 |
\end{description}% |
|
18543 | 123 |
\end{isamarkuptext}% |
124 |
\isamarkuptrue% |
|
125 |
% |
|
24089 | 126 |
\isamarkupsection{Thread-safe programming% |
127 |
} |
|
128 |
\isamarkuptrue% |
|
129 |
% |
|
130 |
\begin{isamarkuptext}% |
|
131 |
Recent versions of Poly/ML (5.1 or later) support multithreaded |
|
132 |
execution based on native operating system threads of the |
|
133 |
underlying platform. Thus threads will actually be executed in |
|
134 |
parallel on multi-core systems. A speedup-factor of approximately |
|
135 |
2--4 can be expected for large well-structured Isabelle sessions, |
|
136 |
where theories are organized as a graph with sufficiently many |
|
137 |
independent nodes. |
|
138 |
||
139 |
Threads lack the memory protection of separate processes, but |
|
140 |
operate concurrently on shared heap memory. This has the advantage |
|
141 |
that results of independent computations are immediately available |
|
142 |
to other threads, without requiring explicit communication, |
|
143 |
reloading, or even recoding of data. |
|
144 |
||
145 |
On the other hand, some programming guidelines need to be observed |
|
146 |
in order to make unprotected parallelism work out smoothly. While |
|
147 |
the ML system implementation is responsible to maintain basic |
|
148 |
integrity of the representation of ML values in memory, the |
|
149 |
application programmer needs to ensure that multithreaded execution |
|
150 |
does not break the intended semantics. |
|
151 |
||
152 |
\medskip \paragraph{Critical shared resources.} Actually only those |
|
153 |
parts outside the purely functional world of ML are critical. In |
|
154 |
particular, this covers |
|
155 |
||
156 |
\begin{itemize} |
|
157 |
||
158 |
\item global references (or arrays), i.e.\ those that persist over |
|
159 |
several invocations of associated operations,\footnote{This is |
|
160 |
independent of the visibility of such mutable values in the toplevel |
|
161 |
scope.} |
|
162 |
||
163 |
\item global ML bindings in the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to |
|
164 |
run-time invocation of the compiler, |
|
165 |
||
166 |
\item direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}. |
|
167 |
||
168 |
\end{itemize} |
|
169 |
||
170 |
The majority of tools implemented within the Isabelle/Isar framework |
|
171 |
will not require any of these critical elements: nothing special |
|
172 |
needs to be observed when staying in the purely functional fragment |
|
173 |
of ML. Note that output via the official Isabelle channels does not |
|
174 |
even count as direct I/O in the above sense, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe. |
|
175 |
||
176 |
\paragraph{Multithreading in Isabelle/Isar.} Our parallel execution |
|
177 |
model is centered around the theory loader. Whenever a given |
|
178 |
subgraph of theories needs to be updated, the system schedules a |
|
179 |
number of threads to process the sources as required, while |
|
180 |
observing their dependencies. Thus concurrency is limited to |
|
181 |
independent nodes according to the theory import relation. |
|
182 |
||
183 |
Any user-code that works relatively to the present background theory |
|
184 |
is already safe. Contextual data may be easily stored within the |
|
24090 | 185 |
theory or proof context, thanks to the generic data concept of |
186 |
Isabelle/Isar (see \secref{sec:context-data}). This greatly |
|
24089 | 187 |
diminishes the demand for global state information in the first |
188 |
place. |
|
189 |
||
190 |
\medskip In rare situations where actual mutable content needs to be |
|
191 |
manipulated, Isabelle provides a single \emph{critical section} that |
|
192 |
may be entered while preventing any other thread from doing the |
|
193 |
same. Entering the critical section without contention is very |
|
194 |
fast, and several basic system operations do so frequently. This |
|
195 |
also means that each thread should leave the critical section |
|
196 |
quickly, otherwise parallel execution performance may degrade |
|
197 |
significantly. |
|
198 |
||
199 |
Despite this potential bottle-neck, we refrain from fine-grained |
|
200 |
locking mechanisms: the restriction to a single lock prevents |
|
201 |
deadlocks without demanding further considerations in user programs. |
|
202 |
||
203 |
\paragraph{Good conduct of impure programs.} The following |
|
204 |
guidelines enable non-functional programs to participate in |
|
205 |
multithreading. |
|
206 |
||
207 |
\begin{itemize} |
|
208 |
||
209 |
\item Minimize global state information. Using proper theory and |
|
210 |
proof context data will actually return to functional update of |
|
211 |
values, without any special precautions for multithreading. Apart |
|
212 |
from the fully general functors for theory and proof data (see |
|
213 |
\secref{sec:context-data}) there are drop-in replacements that |
|
24090 | 214 |
emulate primitive references for common cases of \emph{configuration |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24090
diff
changeset
|
215 |
options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24090
diff
changeset
|
216 |
\verb|NamedThmsFun|). |
24089 | 217 |
|
218 |
\item Keep components with local state information |
|
219 |
\emph{re-entrant}. Instead of poking initial values into (private) |
|
220 |
global references, create a new state record on each invocation, and |
|
221 |
pass that through any auxiliary functions of the component. The |
|
222 |
state record may well contain mutable references, without requiring |
|
223 |
any special synchronizations, as long as each invocation sees its |
|
224 |
own copy. Occasionally, one might even return to plain functional |
|
225 |
updates on non-mutable record values here. |
|
226 |
||
227 |
\item Isolate process configuration flags. The main legitimate |
|
228 |
application of global references is to configure the whole process |
|
229 |
in a certain way, essentially affecting all threads. A typical |
|
230 |
example is the \verb|show_types| flag, which tells the pretty printer |
|
231 |
to output explicit type information for terms. Such flags usually |
|
232 |
do not affect the functionality of the core system, but only the |
|
24090 | 233 |
view being presented to the user. |
24089 | 234 |
|
235 |
Occasionally, such global process flags are treated like implicit |
|
236 |
arguments to certain operations, by using the \verb|setmp| combinator |
|
24090 | 237 |
for safe temporary assignment. Its traditional purpose was to |
238 |
ensure proper recovery of the original value when exceptions are |
|
239 |
raised in the body, now the functionality is extended to enter the |
|
240 |
\emph{critical section} (with its usual potential of degrading |
|
241 |
parallelism). |
|
24089 | 242 |
|
243 |
Note that recovery of plain value passing semantics via \verb|setmp|~\isa{ref\ value} assumes that this \isa{ref} is |
|
244 |
exclusively manipulated within the critical section. In particular, |
|
245 |
any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to |
|
246 |
be marked critical as well, to prevent intruding another threads |
|
247 |
local view, and a lost-update in the global scope, too. |
|
248 |
||
249 |
\item Minimize global ML bindings. Processing theories occasionally |
|
250 |
affects the global ML environment as well. While each ML |
|
251 |
compilation unit is safe, the order of scheduling of independent |
|
252 |
declarations might cause problems when composing several modules |
|
253 |
later on, due to hiding of previous ML names. |
|
254 |
||
255 |
This cannot be helped in general, because the ML toplevel lacks the |
|
256 |
graph structure of the Isabelle theory space. Nevertheless, some |
|
257 |
sound conventions of keeping global ML names essentially disjoint |
|
258 |
(e.g.\ with the help of ML structures) prevents the problem to occur |
|
259 |
in most practical situations. |
|
260 |
||
261 |
\end{itemize} |
|
262 |
||
263 |
Recall that in an open ``LCF-style'' system like Isabelle/Isar, the |
|
264 |
user participates in constructing the overall environment. This |
|
24090 | 265 |
means that state-based facilities offered by one component will |
266 |
require special caution later on. So minimizing critical elements, |
|
267 |
by staying within the plain value-oriented view relative to theory |
|
268 |
or proof contexts most of the time, will also reduce the chance of |
|
24089 | 269 |
mishaps occurring to end-users.% |
270 |
\end{isamarkuptext}% |
|
271 |
\isamarkuptrue% |
|
272 |
% |
|
273 |
\isadelimmlref |
|
274 |
% |
|
275 |
\endisadelimmlref |
|
276 |
% |
|
277 |
\isatagmlref |
|
278 |
% |
|
279 |
\begin{isamarkuptext}% |
|
280 |
\begin{mldecls} |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
281 |
\indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\ |
24089 | 282 |
\indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\ |
283 |
\indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\ |
|
284 |
\end{mldecls} |
|
285 |
||
286 |
\begin{description} |
|
287 |
||
288 |
\item \verb|NAMED_CRITICAL|~\isa{name\ f} evaluates \isa{f\ {\isacharparenleft}{\isacharparenright}} |
|
24090 | 289 |
while staying within the critical section of Isabelle/Isar. No |
290 |
other thread may do so at the same time, but non-critical parallel |
|
291 |
execution will continue. The \isa{name} argument serves for |
|
292 |
diagnostic purposes and might help to spot sources of congestion. |
|
24089 | 293 |
|
294 |
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty |
|
295 |
name argument. |
|
296 |
||
297 |
\item \verb|setmp|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x} |
|
298 |
while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily. This recovers a value-passing |
|
299 |
semantics involving global references, regardless of exceptions or |
|
300 |
concurrency. |
|
301 |
||
302 |
\end{description}% |
|
303 |
\end{isamarkuptext}% |
|
304 |
\isamarkuptrue% |
|
305 |
% |
|
306 |
\endisatagmlref |
|
307 |
{\isafoldmlref}% |
|
308 |
% |
|
309 |
\isadelimmlref |
|
310 |
% |
|
311 |
\endisadelimmlref |
|
312 |
% |
|
18543 | 313 |
\isamarkupchapter{Basic library functions% |
314 |
} |
|
315 |
\isamarkuptrue% |
|
316 |
% |
|
317 |
\begin{isamarkuptext}% |
|
22293 | 318 |
Beyond the proposal of the SML/NJ basis library, Isabelle comes |
319 |
with its own library, from which selected parts are given here. |
|
26459 | 320 |
These should encourage a study of the Isabelle sources, |
321 |
in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.% |
|
22293 | 322 |
\end{isamarkuptext}% |
323 |
\isamarkuptrue% |
|
324 |
% |
|
325 |
\isamarkupsection{Linear transformations% |
|
326 |
} |
|
327 |
\isamarkuptrue% |
|
328 |
% |
|
329 |
\isadelimmlref |
|
330 |
% |
|
331 |
\endisadelimmlref |
|
332 |
% |
|
333 |
\isatagmlref |
|
334 |
% |
|
335 |
\begin{isamarkuptext}% |
|
336 |
\begin{mldecls} |
|
24089 | 337 |
\indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\ |
22293 | 338 |
\end{mldecls}% |
339 |
\end{isamarkuptext}% |
|
340 |
\isamarkuptrue% |
|
341 |
% |
|
342 |
\endisatagmlref |
|
343 |
{\isafoldmlref}% |
|
344 |
% |
|
345 |
\isadelimmlref |
|
346 |
% |
|
347 |
\endisadelimmlref |
|
348 |
% |
|
22322 | 349 |
\isadelimML |
350 |
% |
|
351 |
\endisadelimML |
|
352 |
% |
|
353 |
\isatagML |
|
354 |
% |
|
355 |
\endisatagML |
|
356 |
{\isafoldML}% |
|
357 |
% |
|
358 |
\isadelimML |
|
359 |
% |
|
360 |
\endisadelimML |
|
361 |
% |
|
22293 | 362 |
\begin{isamarkuptext}% |
26460 | 363 |
\noindent Many problems in functional programming can be thought of |
22322 | 364 |
as linear transformations, i.e.~a caluclation starts with a |
26459 | 365 |
particular value \verb|x : foo| which is then transformed |
366 |
by application of a function \verb|f : foo -> foo|, |
|
367 |
continued by an application of a function \verb|g : foo -> bar|, |
|
25151 | 368 |
and so on. As a canoncial example, take functions enriching |
369 |
a theory by constant declararion and primitive definitions: |
|
370 |
||
26459 | 371 |
\smallskip\begin{mldecls} |
28110 | 372 |
\verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix|\isasep\isanewline% |
26459 | 373 |
\verb| -> theory -> term * theory| \\ |
374 |
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory| |
|
375 |
\end{mldecls} |
|
25151 | 376 |
|
26460 | 377 |
\noindent Written with naive application, an addition of constant |
25151 | 378 |
\isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and |
26459 | 379 |
a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like: |
25151 | 380 |
|
26459 | 381 |
\smallskip\begin{mldecls} |
382 |
\verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline% |
|
25151 | 383 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline% |
384 |
\verb| (Sign.declare_const []|\isasep\isanewline% |
|
28110 | 385 |
\verb| ((Name.binding "bar", @{typ "foo => foo"}), NoSyn) thy)| |
26459 | 386 |
\end{mldecls} |
25151 | 387 |
|
26460 | 388 |
\noindent With increasing numbers of applications, this code gets quite |
25151 | 389 |
unreadable. Further, it is unintuitive that things are |
390 |
written down in the opposite order as they actually ``happen''.% |
|
22322 | 391 |
\end{isamarkuptext}% |
392 |
\isamarkuptrue% |
|
393 |
% |
|
394 |
\begin{isamarkuptext}% |
|
25151 | 395 |
\noindent At this stage, Isabelle offers some combinators which allow |
396 |
for more convenient notation, most notably reverse application: |
|
26459 | 397 |
|
398 |
\smallskip\begin{mldecls} |
|
22322 | 399 |
\verb|thy|\isasep\isanewline% |
28110 | 400 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25151 | 401 |
\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline% |
25608 | 402 |
\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline% |
25151 | 403 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))| |
26459 | 404 |
\end{mldecls}% |
22293 | 405 |
\end{isamarkuptext}% |
406 |
\isamarkuptrue% |
|
407 |
% |
|
408 |
\isadelimmlref |
|
409 |
% |
|
410 |
\endisadelimmlref |
|
411 |
% |
|
412 |
\isatagmlref |
|
413 |
% |
|
414 |
\begin{isamarkuptext}% |
|
415 |
\begin{mldecls} |
|
24089 | 416 |
\indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\ |
417 |
\indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\ |
|
418 |
\indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\ |
|
419 |
\indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\ |
|
25151 | 420 |
\end{mldecls}% |
421 |
\end{isamarkuptext}% |
|
422 |
\isamarkuptrue% |
|
423 |
% |
|
424 |
\endisatagmlref |
|
425 |
{\isafoldmlref}% |
|
426 |
% |
|
427 |
\isadelimmlref |
|
428 |
% |
|
429 |
\endisadelimmlref |
|
430 |
% |
|
431 |
\begin{isamarkuptext}% |
|
432 |
\noindent Usually, functions involving theory updates also return |
|
433 |
side results; to use these conveniently, yet another |
|
434 |
set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->| |
|
435 |
which allows curried access to side results: |
|
26459 | 436 |
|
437 |
\smallskip\begin{mldecls} |
|
25151 | 438 |
\verb|thy|\isasep\isanewline% |
28110 | 439 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25608 | 440 |
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline% |
25151 | 441 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
442 |
||
26459 | 443 |
\end{mldecls} |
25151 | 444 |
|
445 |
\noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own: |
|
26459 | 446 |
|
447 |
\smallskip\begin{mldecls} |
|
25151 | 448 |
\verb|thy|\isasep\isanewline% |
28110 | 449 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25151 | 450 |
\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline% |
25608 | 451 |
\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline% |
25151 | 452 |
|
26459 | 453 |
\end{mldecls} |
25151 | 454 |
|
455 |
\noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation |
|
456 |
in the presence of side results which are left unchanged: |
|
26459 | 457 |
|
458 |
\smallskip\begin{mldecls} |
|
25151 | 459 |
\verb|thy|\isasep\isanewline% |
28110 | 460 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25151 | 461 |
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline% |
25608 | 462 |
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline% |
25151 | 463 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
464 |
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline% |
|
465 |
||
26459 | 466 |
\end{mldecls} |
25151 | 467 |
|
26459 | 468 |
\noindent \verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results: |
469 |
||
470 |
\smallskip\begin{mldecls} |
|
25151 | 471 |
\verb|thy|\isasep\isanewline% |
28110 | 472 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
473 |
\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
|
25608 | 474 |
\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline% |
25151 | 475 |
\verb| ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline% |
476 |
||
26459 | 477 |
\end{mldecls}% |
25151 | 478 |
\end{isamarkuptext}% |
479 |
\isamarkuptrue% |
|
480 |
% |
|
481 |
\isadelimmlref |
|
482 |
% |
|
483 |
\endisadelimmlref |
|
484 |
% |
|
485 |
\isatagmlref |
|
486 |
% |
|
487 |
\begin{isamarkuptext}% |
|
488 |
\begin{mldecls} |
|
489 |
\indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\ |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
490 |
\indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\ |
22293 | 491 |
\end{mldecls}% |
492 |
\end{isamarkuptext}% |
|
493 |
\isamarkuptrue% |
|
494 |
% |
|
22322 | 495 |
\endisatagmlref |
496 |
{\isafoldmlref}% |
|
497 |
% |
|
498 |
\isadelimmlref |
|
499 |
% |
|
500 |
\endisadelimmlref |
|
501 |
% |
|
502 |
\begin{isamarkuptext}% |
|
26459 | 503 |
\noindent This principles naturally lift to \emph{lists} using |
25151 | 504 |
the \verb|fold| and \verb|fold_map| combinators. |
505 |
The first lifts a single function |
|
26459 | 506 |
\begin{quote}\footnotesize |
507 |
\verb|f : 'a -> 'b -> 'b| to \verb|'a list -> 'b -> 'b| |
|
508 |
\end{quote} |
|
25151 | 509 |
such that |
26459 | 510 |
\begin{quote}\footnotesize |
511 |
\verb|y |\verb,|,\verb|> fold f [x1, x2, ..., x_n]| \\ |
|
512 |
\hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb|> f x2 |\verb,|,\verb|> ... |\verb,|,\verb|> f x_n| |
|
513 |
\end{quote} |
|
26460 | 514 |
\noindent The second accumulates side results in a list by lifting |
25151 | 515 |
a single function |
26459 | 516 |
\begin{quote}\footnotesize |
517 |
\verb|f : 'a -> 'b -> 'c * 'b| to \verb|'a list -> 'b -> 'c list * 'b| |
|
518 |
\end{quote} |
|
25151 | 519 |
such that |
26459 | 520 |
\begin{quote}\footnotesize |
521 |
\verb|y |\verb,|,\verb|> fold_map f [x1, x2, ..., x_n]| \\ |
|
522 |
\hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb||\verb,|,\verb|>> f x2 |\verb,|,\verb||\verb,|,\verb|>> ... |\verb,|,\verb||\verb,|,\verb|>> f x_n| \\ |
|
523 |
\hspace*{6ex}\verb||\verb,|,\verb||\verb,|,\verb|> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])| |
|
524 |
\end{quote} |
|
25185 | 525 |
|
26459 | 526 |
\noindent Example: |
527 |
||
528 |
\smallskip\begin{mldecls} |
|
25185 | 529 |
\verb|let|\isasep\isanewline% |
530 |
\verb| val consts = ["foo", "bar"];|\isasep\isanewline% |
|
531 |
\verb|in|\isasep\isanewline% |
|
532 |
\verb| thy|\isasep\isanewline% |
|
533 |
\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline% |
|
28110 | 534 |
\verb| ((Name.binding const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline% |
25185 | 535 |
\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline% |
536 |
\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline% |
|
25608 | 537 |
\verb| Thm.add_def false false ("", def)) defs)|\isasep\isanewline% |
26459 | 538 |
\verb|end| |
539 |
\end{mldecls}% |
|
22322 | 540 |
\end{isamarkuptext}% |
541 |
\isamarkuptrue% |
|
542 |
% |
|
543 |
\isadelimmlref |
|
544 |
% |
|
545 |
\endisadelimmlref |
|
546 |
% |
|
547 |
\isatagmlref |
|
548 |
% |
|
22293 | 549 |
\begin{isamarkuptext}% |
550 |
\begin{mldecls} |
|
24089 | 551 |
\indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\ |
552 |
\indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\ |
|
553 |
\indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\ |
|
554 |
\indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\ |
|
555 |
\indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\ |
|
22293 | 556 |
\end{mldecls}% |
557 |
\end{isamarkuptext}% |
|
558 |
\isamarkuptrue% |
|
559 |
% |
|
22322 | 560 |
\endisatagmlref |
561 |
{\isafoldmlref}% |
|
562 |
% |
|
563 |
\isadelimmlref |
|
564 |
% |
|
565 |
\endisadelimmlref |
|
566 |
% |
|
567 |
\begin{isamarkuptext}% |
|
22550 | 568 |
\noindent All those linear combinators also exist in higher-order |
569 |
variants which do not expect a value on the left hand side |
|
570 |
but a function.% |
|
22322 | 571 |
\end{isamarkuptext}% |
572 |
\isamarkuptrue% |
|
573 |
% |
|
574 |
\isadelimmlref |
|
575 |
% |
|
576 |
\endisadelimmlref |
|
577 |
% |
|
578 |
\isatagmlref |
|
579 |
% |
|
22293 | 580 |
\begin{isamarkuptext}% |
581 |
\begin{mldecls} |
|
24089 | 582 |
\indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\ |
22293 | 583 |
\indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\ |
584 |
\end{mldecls}% |
|
585 |
\end{isamarkuptext}% |
|
586 |
\isamarkuptrue% |
|
587 |
% |
|
588 |
\endisatagmlref |
|
589 |
{\isafoldmlref}% |
|
590 |
% |
|
591 |
\isadelimmlref |
|
592 |
% |
|
593 |
\endisadelimmlref |
|
594 |
% |
|
22550 | 595 |
\begin{isamarkuptext}% |
25185 | 596 |
\noindent These operators allow to ``query'' a context |
597 |
in a series of context transformations: |
|
598 |
||
26459 | 599 |
\smallskip\begin{mldecls} |
25185 | 600 |
\verb|thy|\isasep\isanewline% |
601 |
\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline% |
|
28110 | 602 |
\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline% |
25185 | 603 |
\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline% |
604 |
\verb| (Sign.full_name thy "foobar"))|\isasep\isanewline% |
|
605 |
\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline% |
|
606 |
\verb| else Sign.declare_const []|\isasep\isanewline% |
|
28110 | 607 |
\verb| ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline% |
25185 | 608 |
|
26459 | 609 |
\end{mldecls}% |
22550 | 610 |
\end{isamarkuptext}% |
611 |
\isamarkuptrue% |
|
612 |
% |
|
22293 | 613 |
\isamarkupsection{Options and partiality% |
614 |
} |
|
615 |
\isamarkuptrue% |
|
616 |
% |
|
617 |
\isadelimmlref |
|
618 |
% |
|
619 |
\endisadelimmlref |
|
620 |
% |
|
621 |
\isatagmlref |
|
622 |
% |
|
623 |
\begin{isamarkuptext}% |
|
624 |
\begin{mldecls} |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
625 |
\indexml{is\_some}\verb|is_some: 'a option -> bool| \\ |
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
626 |
\indexml{is\_none}\verb|is_none: 'a option -> bool| \\ |
22293 | 627 |
\indexml{the}\verb|the: 'a option -> 'a| \\ |
628 |
\indexml{these}\verb|these: 'a list option -> 'a list| \\ |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
629 |
\indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\ |
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
630 |
\indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\ |
22293 | 631 |
\indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\ |
632 |
\indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\ |
|
633 |
\end{mldecls}% |
|
634 |
\end{isamarkuptext}% |
|
635 |
\isamarkuptrue% |
|
636 |
% |
|
637 |
\endisatagmlref |
|
638 |
{\isafoldmlref}% |
|
639 |
% |
|
640 |
\isadelimmlref |
|
641 |
% |
|
642 |
\endisadelimmlref |
|
643 |
% |
|
644 |
\begin{isamarkuptext}% |
|
24089 | 645 |
Standard selector functions on \isa{option}s are provided. The |
646 |
\verb|try| and \verb|can| functions provide a convenient interface for |
|
26459 | 647 |
handling exceptions -- both take as arguments a function \verb|f| |
648 |
together with a parameter \verb|x| and handle any exception during |
|
649 |
the evaluation of the application of \verb|f| to \verb|x|, either |
|
24089 | 650 |
return a lifted result (\verb|NONE| on failure) or a boolean value |
651 |
(\verb|false| on failure).% |
|
22293 | 652 |
\end{isamarkuptext}% |
653 |
\isamarkuptrue% |
|
654 |
% |
|
655 |
\isamarkupsection{Common data structures% |
|
656 |
} |
|
657 |
\isamarkuptrue% |
|
658 |
% |
|
659 |
\isamarkupsubsection{Lists (as set-like data structures)% |
|
660 |
} |
|
661 |
\isamarkuptrue% |
|
662 |
% |
|
663 |
\begin{isamarkuptext}% |
|
664 |
\begin{mldecls} |
|
665 |
\indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\ |
|
666 |
\indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\ |
|
667 |
\indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\ |
|
668 |
\indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\ |
|
669 |
\end{mldecls}% |
|
670 |
\end{isamarkuptext}% |
|
671 |
\isamarkuptrue% |
|
672 |
% |
|
673 |
\begin{isamarkuptext}% |
|
22503 | 674 |
Lists are often used as set-like data structures -- set-like in |
25151 | 675 |
the sense that they support a notion of \verb|member|-ship, |
22503 | 676 |
\verb|insert|-ing and \verb|remove|-ing, but are order-sensitive. |
677 |
This is convenient when implementing a history-like mechanism: |
|
678 |
\verb|insert| adds an element \emph{to the front} of a list, |
|
679 |
if not yet present; \verb|remove| removes \emph{all} occurences |
|
680 |
of a particular element. Correspondingly \verb|merge| implements a |
|
681 |
a merge on two lists suitable for merges of context data |
|
682 |
(\secref{sec:context-theory}). |
|
683 |
||
684 |
Functions are parametrized by an explicit equality function |
|
685 |
to accomplish overloaded equality; in most cases of monomorphic |
|
24089 | 686 |
equality, writing \verb|op =| should suffice.% |
22293 | 687 |
\end{isamarkuptext}% |
688 |
\isamarkuptrue% |
|
689 |
% |
|
690 |
\isamarkupsubsection{Association lists% |
|
691 |
} |
|
692 |
\isamarkuptrue% |
|
693 |
% |
|
694 |
\begin{isamarkuptext}% |
|
695 |
\begin{mldecls} |
|
696 |
\indexmlexception{AList.DUP}\verb|exception AList.DUP| \\ |
|
697 |
\indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\ |
|
698 |
\indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\ |
|
699 |
\indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\ |
|
700 |
\indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\ |
|
701 |
\indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\ |
|
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
702 |
\indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline% |
22293 | 703 |
\verb| -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\ |
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
704 |
\indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline% |
22293 | 705 |
\verb| -> ('a * 'b) list -> ('a * 'b) list| \\ |
706 |
\indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline% |
|
707 |
\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\ |
|
708 |
\indexml{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline% |
|
709 |
\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| |
|
710 |
\end{mldecls}% |
|
711 |
\end{isamarkuptext}% |
|
712 |
\isamarkuptrue% |
|
713 |
% |
|
714 |
\begin{isamarkuptext}% |
|
22503 | 715 |
Association lists can be seens as an extension of set-like lists: |
716 |
on the one hand, they may be used to implement finite mappings, |
|
717 |
on the other hand, they remain order-sensitive and allow for |
|
718 |
multiple key-value-pair with the same key: \verb|AList.lookup| |
|
719 |
returns the \emph{first} value corresponding to a particular |
|
720 |
key, if present. \verb|AList.update| updates |
|
721 |
the \emph{first} occurence of a particular key; if no such |
|
722 |
key exists yet, the key-value-pair is added \emph{to the front}. |
|
723 |
\verb|AList.delete| only deletes the \emph{first} occurence of a key. |
|
724 |
\verb|AList.merge| provides an operation suitable for merges of context data |
|
725 |
(\secref{sec:context-theory}), where an equality parameter on |
|
726 |
values determines whether a merge should be considered a conflict. |
|
727 |
A slightly generalized operation if implementend by the \verb|AList.join| |
|
728 |
function which allows for explicit conflict resolution.% |
|
22293 | 729 |
\end{isamarkuptext}% |
730 |
\isamarkuptrue% |
|
731 |
% |
|
732 |
\isamarkupsubsection{Tables% |
|
733 |
} |
|
734 |
\isamarkuptrue% |
|
735 |
% |
|
736 |
\begin{isamarkuptext}% |
|
737 |
\begin{mldecls} |
|
738 |
\indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\ |
|
23653 | 739 |
\indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\ |
22293 | 740 |
\indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\ |
23653 | 741 |
\indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\ |
22293 | 742 |
\indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\ |
23653 | 743 |
\indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\ |
744 |
\indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\ |
|
745 |
\indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\ |
|
746 |
\indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\ |
|
747 |
\indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline% |
|
22293 | 748 |
\verb| -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\ |
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
749 |
\indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline% |
22293 | 750 |
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\ |
26854
9b4aec46ad78
improved treatment of "_" thanks to underscore.sty;
wenzelm
parents:
26460
diff
changeset
|
751 |
\indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline% |
22293 | 752 |
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\ |
23653 | 753 |
\indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline% |
22293 | 754 |
\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline% |
23653 | 755 |
\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| \\ |
22293 | 756 |
\indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline% |
757 |
\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline% |
|
23653 | 758 |
\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| |
22293 | 759 |
\end{mldecls}% |
760 |
\end{isamarkuptext}% |
|
761 |
\isamarkuptrue% |
|
762 |
% |
|
763 |
\begin{isamarkuptext}% |
|
22503 | 764 |
Tables are an efficient representation of finite mappings without |
765 |
any notion of order; due to their efficiency they should be used |
|
766 |
whenever such pure finite mappings are neccessary. |
|
767 |
||
768 |
The key type of tables must be given explicitly by instantiating |
|
769 |
the \verb|TableFun| functor which takes the key type |
|
770 |
together with its \verb|order|; for convience, we restrict |
|
771 |
here to the \verb|Symtab| instance with \verb|string| |
|
772 |
as key type. |
|
773 |
||
774 |
Most table functions correspond to those of association lists.% |
|
18543 | 775 |
\end{isamarkuptext}% |
776 |
\isamarkuptrue% |
|
777 |
% |
|
778 |
\isadelimtheory |
|
779 |
% |
|
780 |
\endisadelimtheory |
|
781 |
% |
|
782 |
\isatagtheory |
|
783 |
\isacommand{end}\isamarkupfalse% |
|
18537 | 784 |
% |
785 |
\endisatagtheory |
|
786 |
{\isafoldtheory}% |
|
787 |
% |
|
788 |
\isadelimtheory |
|
789 |
% |
|
790 |
\endisadelimtheory |
|
18543 | 791 |
\isanewline |
18537 | 792 |
\end{isabellebody}% |
793 |
%%% Local Variables: |
|
794 |
%%% mode: latex |
|
795 |
%%% TeX-master: "root" |
|
796 |
%%% End: |