doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 26840 ec46381f149d
child 26849 df50bc1249d7
equal deleted inserted replaced
26839:1d963bfd4a1b 26840:ec46381f149d
       
     1 %
       
     2 \begin{isabellebody}%
       
     3 \def\isabellecontext{HOL{\isacharunderscore}Specific}%
       
     4 %
       
     5 \isadelimtheory
       
     6 \isanewline
       
     7 \isanewline
       
     8 %
       
     9 \endisadelimtheory
       
    10 %
       
    11 \isatagtheory
       
    12 \isacommand{theory}\isamarkupfalse%
       
    13 \ HOL{\isacharunderscore}Specific\isanewline
       
    14 \isakeyword{imports}\ HOL\isanewline
       
    15 \isakeyword{begin}\isanewline
       
    16 \isanewline
       
    17 \isacommand{end}\isamarkupfalse%
       
    18 %
       
    19 \endisatagtheory
       
    20 {\isafoldtheory}%
       
    21 %
       
    22 \isadelimtheory
       
    23 \isanewline
       
    24 %
       
    25 \endisadelimtheory
       
    26 \end{isabellebody}%
       
    27 %%% Local Variables:
       
    28 %%% mode: latex
       
    29 %%% TeX-master: "root"
       
    30 %%% End: