# 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) \ 12" value [code] "(10::int) \ 12" -value [SML] "(10::int) \ 12" value [nbe] "(10::int) \ 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