diff -r 6efe70ab7add -r 6f162dd72f60 src/HOL/ex/CodeEval.thy --- 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) = []" *}