doc-src/TutorialI/Inductive/document/Even.tex
changeset 16523 f8a734dc0fbc
parent 16069 3f2a9f400168
child 17056 05fc32a23b8b
equal deleted inserted replaced
16522:f718767efd49 16523:f8a734dc0fbc
     1 %
     1 %
     2 \begin{isabellebody}%
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Even}%
     3 \def\isabellecontext{Even}%
     4 \isanewline
     4 \isanewline
     5 \isacommand{theory}\ Even\ {\isacharequal}\ Main{\isacharcolon}\isanewline
     5 \isacommand{theory}\ Even\ \isakeyword{imports}\ Main\ \isakeyword{begin}\isanewline
     6 \isanewline
     6 \isanewline
     7 \isanewline
     7 \isanewline
     8 \isamarkupfalse%
     8 \isamarkupfalse%
     9 \isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline
     9 \isacommand{consts}\ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ set{\isachardoublequote}\isanewline
    10 \isamarkupfalse%
    10 \isamarkupfalse%