What is Isabelle/HOL command for Compute in Coq?

Question

Proof assistant Coq have compute command (and also check command for determination of the type) which returns the result of function application. Does Isabelle/HOL have similar command and how it is named?

Answer 1

Isabelle has a "value" command that performs evaluation.

value "rev [1::nat,2,3]"

Isabelle then responds with:

"[Suc (Suc (Suc 0)), Suc (Suc 0), Suc 0]"
  :: "nat list"

(Quoted from https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2007-October/msg00008.html)