| changeset 10362 | c6b197ccf1f1 |
| parent 9933 | 9feb1e0c4cb3 |
| child 10654 | 458068404143 |
--- a/doc-src/TutorialI/Recdef/examples.thy Mon Oct 30 18:28:00 2000 +0100 +++ b/doc-src/TutorialI/Recdef/examples.thy Tue Oct 31 08:53:12 2000 +0100 @@ -69,7 +69,7 @@ *} consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"; recdef sep2 "measure length" - "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)" + "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)" "sep2 xs = (\<lambda>a. xs)"; text{*