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;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{locale}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 \isanewline
     8 \isanewline
     9 %
    10 \endisadelimtheory
    11 %
    12 \isatagtheory
    13 \isacommand{theory}\isamarkupfalse%
    14 \ {\isachardoublequoteopen}locale{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
    15 \endisatagtheory
    16 {\isafoldtheory}%
    17 %
    18 \isadelimtheory
    19 %
    20 \endisadelimtheory
    21 %
    22 \isamarkupchapter{Structured specifications%
    23 }
    24 \isamarkuptrue%
    25 %
    26 \isamarkupsection{Specification elements%
    27 }
    28 \isamarkuptrue%
    29 %
    30 \begin{isamarkuptext}%
    31 FIXME%
    32 \end{isamarkuptext}%
    33 \isamarkuptrue%
    34 %
    35 \isamarkupsection{Type-checking specifications%
    36 }
    37 \isamarkuptrue%
    38 %
    39 \begin{isamarkuptext}%
    40 FIXME%
    41 \end{isamarkuptext}%
    42 \isamarkuptrue%
    43 %
    44 \isamarkupsection{Local theories%
    45 }
    46 \isamarkuptrue%
    47 %
    48 \begin{isamarkuptext}%
    49 FIXME
    50 
    51   \glossary{Local theory}{FIXME}%
    52 \end{isamarkuptext}%
    53 \isamarkuptrue%
    54 %
    55 \isadelimtheory
    56 %
    57 \endisadelimtheory
    58 %
    59 \isatagtheory
    60 \isacommand{end}\isamarkupfalse%
    61 %
    62 \endisatagtheory
    63 {\isafoldtheory}%
    64 %
    65 \isadelimtheory
    66 %
    67 \endisadelimtheory
    68 \isanewline
    69 \end{isabellebody}%
    70 %%% Local Variables:
    71 %%% mode: latex
    72 %%% TeX-master: "root"
    73 %%% End: