1.1 --- a/doc-src/TutorialI/Inductive/Star.thy	Thu Jul 19 15:33:27 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/Star.thy	Thu Jul 19 15:35:00 2007 +0200
     1.3 @@ -54,8 +54,8 @@
     1.4  To prove transitivity, we need rule induction, i.e.\ theorem
     1.5  @{thm[source]rtc.induct}:
     1.6  @{thm[display]rtc.induct}
     1.7 -It says that @{text"?P"} holds for an arbitrary pair @{text"(?xb,?xa) \<in>
     1.8 -?r*"} if @{text"?P"} is preserved by all rules of the inductive definition,
     1.9 +It says that @{text"?P"} holds for an arbitrary pair @{thm_style prem1 rtc.induct}
    1.10 +if @{text"?P"} is preserved by all rules of the inductive definition,
    1.11  i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the
    1.12  premises. In general, rule induction for an $n$-ary inductive relation $R$
    1.13  expects a premise of the form $(x@1,\dots,x@n) \in R$.