CookBook/Package/Ind_Examples.thy
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))