doc-src/TutorialI/Datatype/document/unfoldnested.tex
changeset 48519 5deda0549f97
parent 48518 0c86acc069ad
child 48520 6d4ea2efa64b
equal deleted inserted replaced
48518:0c86acc069ad 48519:5deda0549f97
     1 %
       
     2 \begin{isabellebody}%
       
     3 \def\isabellecontext{unfoldnested}%
       
     4 %
       
     5 \isadelimtheory
       
     6 %
       
     7 \endisadelimtheory
       
     8 %
       
     9 \isatagtheory
       
    10 %
       
    11 \endisatagtheory
       
    12 {\isafoldtheory}%
       
    13 %
       
    14 \isadelimtheory
       
    15 %
       
    16 \endisadelimtheory
       
    17 \isacommand{datatype}\isamarkupfalse%
       
    18 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{5F}{\isacharunderscore}}list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
       
    19 \isakeyword{and}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{5F}{\isacharunderscore}}list{\isaliteral{22}{\isachardoublequoteclose}}%
       
    20 \isadelimtheory
       
    21 %
       
    22 \endisadelimtheory
       
    23 %
       
    24 \isatagtheory
       
    25 %
       
    26 \endisatagtheory
       
    27 {\isafoldtheory}%
       
    28 %
       
    29 \isadelimtheory
       
    30 %
       
    31 \endisadelimtheory
       
    32 \end{isabellebody}%
       
    33 %%% Local Variables:
       
    34 %%% mode: latex
       
    35 %%% TeX-master: "root"
       
    36 %%% End: