# HG changeset patch # User nipkow # Date 989480505 -7200 # Node ID d838df8795853dec12faff2452ec0a9cea0fe1b9 # Parent 02db0084a695b923f1ba7c7a98ba27c0e3b0ae93 *** empty log message *** diff -r 02db0084a695 -r d838df879585 doc-src/TutorialI/Overview/FP1.thy --- a/doc-src/TutorialI/Overview/FP1.thy Wed May 09 23:09:26 2001 +0200 +++ b/doc-src/TutorialI/Overview/FP1.thy Thu May 10 09:41:45 2001 +0200 @@ -123,7 +123,7 @@ apply simp oops -lemma "case xs @ [] of [] \ A | y#ys \ B"; +lemma "case xs @ [] of [] \ P | y#ys \ Q ys y"; apply simp apply(simp split: list.split) oops