1.1 --- a/doc-src/TutorialI/Inductive/Even.thy	Mon Jul 23 14:36:37 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/Even.thy	Mon Jul 23 14:39:21 2007 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  subsection{* Making an Inductive Definition *}
     1.5  
     1.6  text {*
     1.7 -Using \commdx{inductive\_set}, we declare the constant @{text even} to be
     1.8 +Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be
     1.9  a set of natural numbers with the desired properties.
    1.10  *}
    1.11  

     2.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jul 23 14:36:37 2007 +0200
     2.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jul 23 14:39:21 2007 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4  \isamarkuptrue%
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -Using \commdx{inductive\_set}, we declare the constant \isa{even} to be
     2.8 +Using \commdx{inductive\protect\_set}, we declare the constant \isa{even} to be
     2.9  a set of natural numbers with the desired properties.%
    2.10  \end{isamarkuptext}%
    2.11  \isamarkuptrue%