| changeset 22319 | 6f162dd72f60 |
| parent 22017 | 9b1656a28c88 |
| child 22333 | 652f316ca26a |
--- a/src/HOL/ex/CodeEval.thy Wed Feb 14 10:06:14 2007 +0100 +++ b/src/HOL/ex/CodeEval.thy Wed Feb 14 10:06:15 2007 +0100 @@ -154,6 +154,7 @@ subsection {* Small examples *} +ML {* Eval.term "(Suc 2 + 1) * 4" *} ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *} ML {* Eval.term "[]::nat list" *} ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *}