doc-src/IsarImplementation/Thy/document/locale.tex
changeset 30101 5c6efec476ae
parent 30100 e1c714d33c5c
parent 29777 f3284860004c
child 30105 37f47ea6fed1
equal deleted inserted replaced
30100:e1c714d33c5c 30101:5c6efec476ae
     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: