--- a/doc-src/TutorialI/Inductive/Star.thy Thu Jun 12 14:46:15 2008 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy Thu Jun 12 15:49:25 2008 +0200
@@ -84,7 +84,7 @@
depend on its second parameter at all. The reason is that in our original
goal, of the pair @{term"(x,y)"} only @{term x} appears also in the
conclusion, but not @{term y}. Thus our induction statement is too
-weak. Fortunately, it can easily be strengthened:
+general. Fortunately, it can easily be specialized:
transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*}
(*<*)oops(*>*)
lemma rtc_trans[rule_format]: