diff -r 5a6935d598c3 -r 6cd88d27f600 src/HOL/ex/Eval_examples.thy
--- 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 *}