summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Thu, 19 Jul 2007 15:35:00 +0200 | |

changeset 23847 | 32d76edc5e5c |

parent 23846 | bfedd1a024fc |

child 23848 | ca73e86c22bb |

Refer to major premise of induction rule via "thm_style prem1".

--- 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$.