doc-src/IsarRef/Thy/document/HOL_Specific.tex
author wenzelm
Wed May 07 12:38:55 2008 +0200 (2008-05-07)
changeset 26840 ec46381f149d
child 26849 df50bc1249d7
permissions -rw-r--r--
added logic-specific sessions;
     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: