doc-src/IsarImplementation/Thy/document/Syntax.tex
changeset 30242 aea5d7fa7ef5
parent 30124 b956bf0dc87c
child 35001 31f8d9eaceff
equal deleted inserted replaced
30241:3a1aef73b2b2 30242:aea5d7fa7ef5
       
     1 %
       
     2 \begin{isabellebody}%
       
     3 \def\isabellecontext{Syntax}%
       
     4 %
       
     5 \isadelimtheory
       
     6 %
       
     7 \endisadelimtheory
       
     8 %
       
     9 \isatagtheory
       
    10 \isacommand{theory}\isamarkupfalse%
       
    11 \ Syntax\isanewline
       
    12 \isakeyword{imports}\ Base\isanewline
       
    13 \isakeyword{begin}%
       
    14 \endisatagtheory
       
    15 {\isafoldtheory}%
       
    16 %
       
    17 \isadelimtheory
       
    18 %
       
    19 \endisadelimtheory
       
    20 %
       
    21 \isamarkupchapter{Syntax and type-checking%
       
    22 }
       
    23 \isamarkuptrue%
       
    24 %
       
    25 \begin{isamarkuptext}%
       
    26 FIXME%
       
    27 \end{isamarkuptext}%
       
    28 \isamarkuptrue%
       
    29 %
       
    30 \isadelimtheory
       
    31 %
       
    32 \endisadelimtheory
       
    33 %
       
    34 \isatagtheory
       
    35 \isacommand{end}\isamarkupfalse%
       
    36 %
       
    37 \endisatagtheory
       
    38 {\isafoldtheory}%
       
    39 %
       
    40 \isadelimtheory
       
    41 %
       
    42 \endisadelimtheory
       
    43 \isanewline
       
    44 \end{isabellebody}%
       
    45 %%% Local Variables:
       
    46 %%% mode: latex
       
    47 %%% TeX-master: "root"
       
    48 %%% End: