diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Package/Ind_Examples.thy --- 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 "(\x. P x x) \ (\x y z. R x y \ P y z \ P x z) \ P x y" apply(atomize (full))