| changeset 23928 | efee34ff4764 |
| parent 23842 | 9d87177f1f89 |
| child 25330 | 15bf0f47a87d |
--- a/doc-src/TutorialI/Inductive/Even.thy Mon Jul 23 14:36:37 2007 +0200 +++ b/doc-src/TutorialI/Inductive/Even.thy Mon Jul 23 14:39:21 2007 +0200 @@ -16,7 +16,7 @@ subsection{* Making an Inductive Definition *} text {* -Using \commdx{inductive\_set}, we declare the constant @{text even} to be +Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be a set of natural numbers with the desired properties. *}