Coq 中用于计算的 Isabelle/HOL 命令是什么？

Question

证明助手Coq有compute命令（还有check类型判断命令）返回函数应用的结果。 Isabelle/HOL 是否有类似的命令以及如何命名？

Answer 1

Isabelle 有一个执行评估的“值”命令。

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

伊莎贝尔随后回应：

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

（引自https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2007-October/msg00008.html）