[isabelle] Isabelle problem

["Beta Ziliani" <beta.ziliani at gmail.com>]

Dear Isabelle User Group:

  I've this problem using X-Isabelle. I've just downloaded Isabelle, with
Emacs 21.4.20 in a Kubuntu 7.10. Looking at the tutorial I put this simple
excercise

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

But whenever I want to do something useful , like use the command (by
pressing the Command  button in the Proof General Toolbar)

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

Isabelle respond with a
*** Illegal application of command "value" at top level
*** At command "value".

I'm making things wrong, or my installation is wrong?

Thanks in advance,
Beta