src/HOL/ex/Eval_Examples.thy

--- a/src/HOL/ex/Eval_Examples.thy	Thu Sep 20 16:37:30 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Thu Sep 20 16:37:31 2007 +0200
@@ -5,7 +5,7 @@
 header {* Small examples for evaluation mechanisms *}
 
 theory Eval_Examples
-imports Eval
+imports Eval "~~/src/HOL/Real/Rational"
 begin
 
 text {* SML evaluation oracle *}
@@ -34,6 +34,8 @@
 value "[]::nat list"
 value "[(nat 100, ())]"
 value "max (2::int) 4"
+value "of_int 2 / of_int 4 * (1::rat)"
+
 
 text {* a fancy datatype *}