| changeset 21117 | e8657a20a52f |
| parent 20835 | 27d049062b56 |
| child 21154 | c8cc6b68759f |
--- a/src/HOL/ex/CodeEval.thy Tue Oct 31 09:29:06 2006 +0100 +++ b/src/HOL/ex/CodeEval.thy Tue Oct 31 09:29:08 2006 +0100 @@ -180,8 +180,8 @@ subsection {* Small examples *} +ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *} ML {* Eval.term "[]::nat list" *} -ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *} ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *} text {* a fancy datatype *}