# HG changeset patch
# User berghofe
# Date 1185194361 -7200
# Node ID efee34ff4764096bd55bf8f548ba6a68c401c601
# Parent  cbe0e4aeb53cb4047c67278def3049c2d83f14ff
Protected underscore in inductive_set.

diff -r cbe0e4aeb53c -r efee34ff4764 doc-src/TutorialI/Inductive/Even.thy
--- 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.
 *}
 
diff -r cbe0e4aeb53c -r efee34ff4764 doc-src/TutorialI/Inductive/document/Even.tex
--- a/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jul 23 14:36:37 2007 +0200
+++ b/doc-src/TutorialI/Inductive/document/Even.tex	Mon Jul 23 14:39:21 2007 +0200
@@ -35,7 +35,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Using \commdx{inductive\_set}, we declare the constant \isa{even} to be
+Using \commdx{inductive\protect\_set}, we declare the constant \isa{even} to be
 a set of natural numbers with the desired properties.%
 \end{isamarkuptext}%
 \isamarkuptrue%