# HG changeset patch
# User bulwahn
# Date 1312374263 -7200
# Node ID 2d633b795d4aec629c4367ba70fba58ea1a5decf
# Parent  7c39c83002b96ff9fd29c353bdd986fb8329f0b3
removing value invocations with the SML code generator

diff -r 7c39c83002b9 -r 2d633b795d4a src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Wed Aug 03 13:59:59 2011 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Wed Aug 03 14:24:23 2011 +0200
@@ -34,42 +34,34 @@
 
 value "(Suc 2 + 1) * 4"
 value [code] "(Suc 2 + 1) * 4"
-value [SML] "(Suc 2 + 1) * 4"
 value [nbe] "(Suc 2 + 1) * 4"
 
 value "(Suc 2 + Suc 0) * Suc 3"
 value [code] "(Suc 2 + Suc 0) * Suc 3"
-value [SML] "(Suc 2 + Suc 0) * Suc 3"
 value [nbe] "(Suc 2 + Suc 0) * Suc 3"
 
 value "nat 100"
 value [code] "nat 100"
-value [SML] "nat 100"
 value [nbe] "nat 100"
 
 value "(10::int) \<le> 12"
 value [code] "(10::int) \<le> 12"
-value [SML] "(10::int) \<le> 12"
 value [nbe] "(10::int) \<le> 12"
 
 value "max (2::int) 4"
 value [code] "max (2::int) 4"
-value [SML] "max (2::int) 4"
 value [nbe] "max (2::int) 4"
 
 value "of_int 2 / of_int 4 * (1::rat)"
 value [code] "of_int 2 / of_int 4 * (1::rat)"
-value [SML] "of_int 2 / of_int 4 * (1::rat)"
 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
 
 value "[] :: nat list"
 value [code] "[] :: nat list"
-value [SML] "[] :: nat list"
 value [nbe] "[] :: nat list"
 
 value "[(nat 100, ())]"
 value [code] "[(nat 100, ())]"
-value [SML] "[(nat 100, ())]"
 value [nbe] "[(nat 100, ())]"
 
 text {* a fancy datatype *}
@@ -84,7 +76,6 @@
 
 value "Bla (Bar (4::nat) [Suc 0])"
 value [code] "Bla (Bar (4::nat) [Suc 0])"
-value [SML] "Bla (Bar (4::nat) [Suc 0])"
 value [nbe] "Bla (Bar (4::nat) [Suc 0])"
 
 end