more example
authorhaftmann
Wed, 30 May 2007 21:09:16 +0200
changeset 23134 6cd88d27f600
parent 23133 5a6935d598c3
child 23135 9f01af828a10
more example
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 *}