author | haftmann |
Sat, 18 Feb 2012 20:53:39 +0100 | |
changeset 46525 | af3df09590f9 |
parent 43564 | 9864182c6bad |
child 48895 | 4cd4ef1ef4a4 |
permissions | -rw-r--r-- |
30296 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Base}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Base\isanewline |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
30296
diff
changeset
|
12 |
\isakeyword{imports}\ Main\isanewline |
40406 | 13 |
\isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
14 |
\isakeyword{begin}% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
15 |
\endisatagtheory |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
16 |
{\isafoldtheory}% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
17 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
18 |
\isadelimtheory |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
19 |
\isanewline |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
20 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
21 |
\endisadelimtheory |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
22 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
23 |
\isadelimML |
30296 | 24 |
\isanewline |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
25 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
26 |
\endisadelimML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
27 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
28 |
\isatagML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
29 |
\isacommand{setup}\isamarkupfalse% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
30 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
31 |
\endisatagML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
32 |
{\isafoldML}% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
33 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
34 |
\isadelimML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
35 |
\isanewline |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
36 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
37 |
\endisadelimML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
38 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
39 |
\isadelimtheory |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
40 |
\isanewline |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
41 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
42 |
\endisadelimtheory |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
43 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
44 |
\isatagtheory |
30296 | 45 |
\isacommand{end}\isamarkupfalse% |
46 |
% |
|
47 |
\endisatagtheory |
|
48 |
{\isafoldtheory}% |
|
49 |
% |
|
50 |
\isadelimtheory |
|
51 |
\isanewline |
|
52 |
% |
|
53 |
\endisadelimtheory |
|
54 |
\end{isabellebody}% |
|
55 |
%%% Local Variables: |
|
56 |
%%% mode: latex |
|
57 |
%%% TeX-master: "root" |
|
58 |
%%% End: |