# HG changeset patch
# User berghofe
# Date 1184852100 -7200
# Node ID 32d76edc5e5cb523fdfb7a934f01b2e6f285eb51
# Parent  bfedd1a024fc05d721fb06a6fc6373dc5973a257
Refer to major premise of induction rule via "thm_style prem1".

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