| changeset 45015 | fdac1e9880eb |
| parent 43141 | 11fce8564415 |
| child 45265 | 521508e85c0d |
--- a/src/HOL/IMP/Star.thy Tue Sep 20 05:47:11 2011 +0200 +++ b/src/HOL/IMP/Star.thy Tue Sep 20 05:48:23 2011 +0200 @@ -9,7 +9,7 @@ lemma star_trans: "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" -proof(induct rule: star.induct) +proof(induction rule: star.induct) case refl thus ?case . next case step thus ?case by (metis star.step)