| author | paulson |
| Wed, 10 Oct 2007 15:05:34 +0200 | |
| changeset 24942 | 39a23aadc7e1 |
| parent 15141 | a95c2ff210ba |
| child 26729 | 43a72d892594 |
| permissions | -rw-r--r-- |
theory ToyList imports PreList begin datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) rev :: "'a list => 'a list" primrec "[] @ ys = ys" "(x # xs) @ ys = x # (xs @ ys)" primrec "rev [] = []" "rev (x # xs) = (rev xs) @ (x # [])"