doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 42630 a55e0663ad1d
parent 42627 8749742785b8
child 42651 e3fdb7c96be5
equal deleted inserted replaced
42629:f61ac1573ee6 42630:a55e0663ad1d
     8 %
     8 %
     9 \isatagtheory
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    10 \isacommand{theory}\isamarkupfalse%
    11 \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
    11 \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
       
    14 \isakeyword{begin}%
    13 \isakeyword{begin}%
    15 \endisatagtheory
    14 \endisatagtheory
    16 {\isafoldtheory}%
    15 {\isafoldtheory}%
    17 %
    16 %
    18 \isadelimtheory
    17 \isadelimtheory