doc-src/IsarImplementation/Thy/document/locale.tex
changeset 30130 e23770bc97c8
parent 30129 419116f1157a
parent 30114 0726792e1726
child 30131 6be1be402ef0
equal deleted inserted replaced
30129:419116f1157a 30130:e23770bc97c8
     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-inference%
       
    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: