equal
deleted
inserted
replaced
33 \isamarkupsubsection{Making an Inductive Definition% |
33 \isamarkupsubsection{Making an Inductive Definition% |
34 } |
34 } |
35 \isamarkuptrue% |
35 \isamarkuptrue% |
36 % |
36 % |
37 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
38 Using \commdx{inductive\_set}, we declare the constant \isa{even} to be |
38 Using \commdx{inductive\protect\_set}, we declare the constant \isa{even} to be |
39 a set of natural numbers with the desired properties.% |
39 a set of natural numbers with the desired properties.% |
40 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
41 \isamarkuptrue% |
41 \isamarkuptrue% |
42 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
42 \isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% |
43 \ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline |
43 \ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline |