changeset 114 | 13fd0a83d3c3 |
parent 113 | 9b6c9d172378 |
child 115 | 039845fc96bd |
--- a/CookBook/Package/Ind_Examples.thy Fri Feb 13 01:05:31 2009 +0000 +++ b/CookBook/Package/Ind_Examples.thy Fri Feb 13 09:57:08 2009 +0000 @@ -49,7 +49,7 @@ (FIXME: add linenumbers to the proof below and the text above) *} -lemma trcl_induct: +lemma %linenos trcl_induct: assumes asm: "trcl R x y" shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y" apply(atomize (full))