doc-src/IsarImplementation/Thy/document/ML.tex
author wenzelm
Tue, 03 Jan 2006 00:06:23 +0100
changeset 18543 e903a1d0bed5
parent 18537 2681f9e34390
child 18554 bff7a1466fe4
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{ML}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
\isanewline
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
     7
\isanewline
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
     8
\isanewline
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    12
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
\isacommand{theory}\isamarkupfalse%
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    14
\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    15
\endisatagtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    16
{\isafoldtheory}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    17
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    18
\isadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    19
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    20
\endisadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    21
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    22
\isamarkupchapter{Aesthetics of ML programming%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    23
}
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    24
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    25
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    26
\begin{isamarkuptext}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    27
FIXME style guide%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    28
\end{isamarkuptext}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    29
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    30
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    31
\isamarkupchapter{Basic library functions%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    32
}
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    33
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    34
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    35
\begin{isamarkuptext}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    36
FIXME beyond the basis library definition%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    37
\end{isamarkuptext}%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    38
\isamarkuptrue%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    39
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    40
\isadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    41
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    42
\endisadelimtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    43
%
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    44
\isatagtheory
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    45
\isacommand{end}\isamarkupfalse%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    46
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    47
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    48
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    49
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    50
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    51
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    52
\endisadelimtheory
18543
e903a1d0bed5 updated;
wenzelm
parents: 18537
diff changeset
    53
\isanewline
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    54
\end{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    55
%%% Local Variables:
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    56
%%% mode: latex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    57
%%% TeX-master: "root"
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    58
%%% End: