diff -r 6477705ae3ad -r 8236f13be95b doc-src/TutorialI/Inductive/Star.thy --- 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]: