doc-src/IsarImplementation/Thy/document/locale.tex
author wenzelm
Tue Sep 05 16:42:32 2006 +0200 (2006-09-05 ago)
changeset 20477 e623b0e30541
parent 20451 27ea2ba48fa3
child 20520 05fd007bdeb9
permissions -rw-r--r--
tuned;
wenzelm@18537
     1
%
wenzelm@18537
     2
\begin{isabellebody}%
wenzelm@18537
     3
\def\isabellecontext{locale}%
wenzelm@18537
     4
%
wenzelm@18537
     5
\isadelimtheory
wenzelm@18537
     6
\isanewline
wenzelm@18537
     7
\isanewline
wenzelm@18537
     8
\isanewline
wenzelm@18537
     9
%
wenzelm@18537
    10
\endisadelimtheory
wenzelm@18537
    11
%
wenzelm@18537
    12
\isatagtheory
wenzelm@18537
    13
\isacommand{theory}\isamarkupfalse%
wenzelm@18537
    14
\ {\isachardoublequoteopen}locale{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
wenzelm@18537
    15
\endisatagtheory
wenzelm@18537
    16
{\isafoldtheory}%
wenzelm@18537
    17
%
wenzelm@18537
    18
\isadelimtheory
wenzelm@18537
    19
%
wenzelm@18537
    20
\endisadelimtheory
wenzelm@18537
    21
%
wenzelm@18537
    22
\isamarkupchapter{Structured specifications%
wenzelm@18537
    23
}
wenzelm@18537
    24
\isamarkuptrue%
wenzelm@18537
    25
%
wenzelm@18537
    26
\isamarkupsection{Specification elements%
wenzelm@18537
    27
}
wenzelm@18537
    28
\isamarkuptrue%
wenzelm@18537
    29
%
wenzelm@18537
    30
\begin{isamarkuptext}%
wenzelm@18537
    31
FIXME%
wenzelm@18537
    32
\end{isamarkuptext}%
wenzelm@18537
    33
\isamarkuptrue%
wenzelm@18537
    34
%
wenzelm@20451
    35
\isamarkupsection{Type-checking specifications%
wenzelm@18537
    36
}
wenzelm@18537
    37
\isamarkuptrue%
wenzelm@18537
    38
%
wenzelm@18537
    39
\begin{isamarkuptext}%
wenzelm@18537
    40
FIXME%
wenzelm@18537
    41
\end{isamarkuptext}%
wenzelm@18537
    42
\isamarkuptrue%
wenzelm@18537
    43
%
wenzelm@20477
    44
\isamarkupsection{Local theories%
wenzelm@20451
    45
}
wenzelm@20451
    46
\isamarkuptrue%
wenzelm@20451
    47
%
wenzelm@20451
    48
\begin{isamarkuptext}%
wenzelm@20451
    49
FIXME
wenzelm@20451
    50
wenzelm@20451
    51
  \glossary{Local theory}{FIXME}%
wenzelm@20451
    52
\end{isamarkuptext}%
wenzelm@20451
    53
\isamarkuptrue%
wenzelm@20451
    54
%
wenzelm@18537
    55
\isadelimtheory
wenzelm@18537
    56
%
wenzelm@18537
    57
\endisadelimtheory
wenzelm@18537
    58
%
wenzelm@18537
    59
\isatagtheory
wenzelm@18537
    60
\isacommand{end}\isamarkupfalse%
wenzelm@18537
    61
%
wenzelm@18537
    62
\endisatagtheory
wenzelm@18537
    63
{\isafoldtheory}%
wenzelm@18537
    64
%
wenzelm@18537
    65
\isadelimtheory
wenzelm@18537
    66
%
wenzelm@18537
    67
\endisadelimtheory
wenzelm@18537
    68
\isanewline
wenzelm@18537
    69
\end{isabellebody}%
wenzelm@18537
    70
%%% Local Variables:
wenzelm@18537
    71
%%% mode: latex
wenzelm@18537
    72
%%% TeX-master: "root"
wenzelm@18537
    73
%%% End: