equal
deleted
inserted
replaced
14 *} |
14 *} |
15 |
15 |
16 subsection{* Making an Inductive Definition *} |
16 subsection{* Making an Inductive Definition *} |
17 |
17 |
18 text {* |
18 text {* |
19 Using \commdx{inductive\_set}, we declare the constant @{text even} to be |
19 Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be |
20 a set of natural numbers with the desired properties. |
20 a set of natural numbers with the desired properties. |
21 *} |
21 *} |
22 |
22 |
23 inductive_set even :: "nat set" |
23 inductive_set even :: "nat set" |
24 where |
24 where |