| changeset 11292 | d838df879585 |
| parent 11237 | 0ef5ecc1fd4d |
| child 12631 | 7648ac4a6b95 |
--- 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 [] \<Rightarrow> A | y#ys \<Rightarrow> B"; +lemma "case xs @ [] of [] \<Rightarrow> P | y#ys \<Rightarrow> Q ys y"; apply simp apply(simp split: list.split) oops