author | haftmann |
Wed, 30 May 2007 21:09:16 +0200 | |
changeset 23134 | 6cd88d27f600 |
parent 23133 | 5a6935d598c3 |
child 23135 | 9f01af828a10 |
--- a/src/HOL/ex/Eval_examples.thy Wed May 30 21:09:15 2007 +0200 +++ b/src/HOL/ex/Eval_examples.thy Wed May 30 21:09:16 2007 +0200 @@ -20,6 +20,9 @@ value (overloaded) "(Suc 2 + Suc 0) * Suc 3" value (overloaded) "[]::nat list" value (overloaded) "fst ([]::nat list, Suc 0) = []" +value (overloaded) "nat 100" +value (overloaded) "[(nat 100, ())]" +value (overloaded) "int 10 \<le> 12" text {* a fancy datatype *}