author | wenzelm |
Tue, 09 May 2000 16:05:30 +0200 | |
changeset 8846 | c7d945398677 |
parent 8751 | 9ed0548177fb |
child 9541 | d17c0b34d5c8 |
permissions | -rw-r--r-- |
theory ToyList = PreList:; 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 # [])";