diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/Even.thy
--- a/doc-src/TutorialI/Inductive/Even.thy	Wed Jul 11 10:52:20 2007 +0200
+++ b/doc-src/TutorialI/Inductive/Even.thy	Wed Jul 11 10:53:39 2007 +0200
@@ -2,11 +2,10 @@
 theory Even imports Main begin
 
 
-consts even :: "nat set"
-inductive even
-intros
-zero[intro!]: "0 \<in> even"
-step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
+inductive_set even :: "nat set"
+where
+  zero[intro!]: "0 \<in> even"
+| step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even"
 
 text{*An inductive definition consists of introduction rules.