doc-src/TutorialI/Types/Typedefs.thy

--- a/doc-src/TutorialI/Types/Typedefs.thy	Sun Jun 22 23:08:32 2008 +0200
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Mon Jun 23 15:26:47 2008 +0200
@@ -189,9 +189,9 @@
 
 lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x"
 
-txt{*\noindent Again this follows easily from a pre-proved general theorem:*}
+txt{*\noindent Again this follows easily using the induction principle stemming from the type definition:*}
 
-apply(induct_tac x rule: Abs_three_induct)
+apply(induct_tac x)
 
 txt{*
 @{subgoals[display,indent=0]}