--- a/doc-src/TutorialI/Inductive/Even.thy Wed Nov 07 16:43:01 2007 +0100
+++ b/doc-src/TutorialI/Inductive/Even.thy Wed Nov 07 18:19:04 2007 +0100
@@ -20,10 +20,9 @@
a set of natural numbers with the desired properties.
*}
-inductive_set even :: "nat set"
-where
- 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. The first one