# HG changeset patch
# User haftmann
# Date 1180552156 -7200
# Node ID 6cd88d27f600097e959d9a98c4b5d4f1f47f8fc6
# Parent  5a6935d598c3af562c6d81ce5e0bdf6ef5cbd64c
more example

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 *}