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

author | nipkow |

Wed, 30 Oct 2013 17:20:59 +0100 | |

changeset 54217 | 2fa338fd0a28 |

parent 54216 | c0c453ce70a7 |

child 54218 | 07c0c121a8dc |

tuned text

--- a/src/Doc/ProgProve/Logic.thy Tue Oct 29 13:48:18 2013 +0100 +++ b/src/Doc/ProgProve/Logic.thy Wed Oct 30 17:20:59 2013 +0100 @@ -799,12 +799,10 @@ text{* The single @{text r} step is performer after rather than before the @{text star'} -steps. Prove @{prop "star' r x y \<Longrightarrow> star r x y"}. You may need a lemma. -The other direction can also be proved but -you have to be careful how to formulate the lemma it will require: -make sure that the assumption about the inductive predicate -is the first assumption. Assumptions preceding the inductive predicate do not -take part in the induction. +steps. Prove @{prop "star' r x y \<Longrightarrow> star r x y"} and +@{prop "star r x y \<Longrightarrow> star r' x y"}. You may need lemmas. +Note that rule induction fails +if the assumption about the inductive predicate is not the first assumption. \endexercise \ifsem