doc-src/Tutorial/ToyList/ToyList.thy

Removing the datatype declaration of "order" allows the standard General.order
to be used. Thus we can use Int.compare and String.compare instead of the
slower home-grown versions.

ToyList = Datatype +

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 # [])"

end