doc-src/IsarRef/Thy/document/HOLCF_Specific.tex
changeset 42651 e3fdb7c96be5
parent 42596 6c621a9d612a
child 42662 2080fe35abea
equal deleted inserted replaced
42650:552eae49f97d 42651:e3fdb7c96be5
     7 \endisadelimtheory
     7 \endisadelimtheory
     8 %
     8 %
     9 \isatagtheory
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    10 \isacommand{theory}\isamarkupfalse%
    11 \ HOLCF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
    11 \ HOLCF{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
    12 \isakeyword{imports}\ HOLCF\isanewline
    12 \isakeyword{imports}\ Base\ HOLCF\isanewline
    13 \isakeyword{begin}%
    13 \isakeyword{begin}%
    14 \endisatagtheory
    14 \endisatagtheory
    15 {\isafoldtheory}%
    15 {\isafoldtheory}%
    16 %
    16 %
    17 \isadelimtheory
    17 \isadelimtheory