canonical 'cases'/'induct' rules for n-tuples (n=3..7)
(really belongs to theory Product_Type, but doesn't work there yet)
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