[isabelle] solving error



Hi,
I began to read Isabelle tutorial. I proceed
program bellow step by step, but it show
me error. Does anybody know how to
solve it?
Thanks

ERROR
*** Inner lexical error at: @ ys = ys
*** Failed to parse proposition
*** At command "primrec".

PROGRAM
theory ToyList
imports Datatype
begin

datatype 'a list = Nil
| Cons 'a "'a list"

primrec app :: "'a list => 'a list => 'a list"
where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"

primrec rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"

value "rev (True # False # [])"
end





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.