src/HOL/ex/Eval_Examples.thy
changeset 28227 77221ee0f7b9
parent 26020 ffe1a032d24b
child 28952 15a4b2cf8c34
     1.1 --- a/src/HOL/ex/Eval_Examples.thy	Mon Sep 15 20:51:58 2008 +0200
     1.2 +++ b/src/HOL/ex/Eval_Examples.thy	Tue Sep 16 09:21:22 2008 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Small examples for evaluation mechanisms *}
     1.5  
     1.6  theory Eval_Examples
     1.7 -imports Eval "~~/src/HOL/Real/Rational"
     1.8 +imports Code_Eval "~~/src/HOL/Real/Rational"
     1.9  begin
    1.10  
    1.11  text {* evaluation oracle *}
    1.12 @@ -35,44 +35,44 @@
    1.13  text {* term evaluation *}
    1.14  
    1.15  value "(Suc 2 + 1) * 4"
    1.16 -value (code) "(Suc 2 + 1) * 4"
    1.17 -value (SML) "(Suc 2 + 1) * 4"
    1.18 -value ("normal_form") "(Suc 2 + 1) * 4"
    1.19 +value [code] "(Suc 2 + 1) * 4"
    1.20 +value [SML] "(Suc 2 + 1) * 4"
    1.21 +value [nbe] "(Suc 2 + 1) * 4"
    1.22  
    1.23  value "(Suc 2 + Suc 0) * Suc 3"
    1.24 -value (code) "(Suc 2 + Suc 0) * Suc 3"
    1.25 -value (SML) "(Suc 2 + Suc 0) * Suc 3"
    1.26 -value ("normal_form") "(Suc 2 + Suc 0) * Suc 3"
    1.27 +value [code] "(Suc 2 + Suc 0) * Suc 3"
    1.28 +value [SML] "(Suc 2 + Suc 0) * Suc 3"
    1.29 +value [nbe] "(Suc 2 + Suc 0) * Suc 3"
    1.30  
    1.31  value "nat 100"
    1.32 -value (code) "nat 100"
    1.33 -value (SML) "nat 100"
    1.34 -value ("normal_form") "nat 100"
    1.35 +value [code] "nat 100"
    1.36 +value [SML] "nat 100"
    1.37 +value [nbe] "nat 100"
    1.38  
    1.39  value "(10\<Colon>int) \<le> 12"
    1.40 -value (code) "(10\<Colon>int) \<le> 12"
    1.41 -value (SML) "(10\<Colon>int) \<le> 12"
    1.42 -value ("normal_form") "(10\<Colon>int) \<le> 12"
    1.43 +value [code] "(10\<Colon>int) \<le> 12"
    1.44 +value [SML] "(10\<Colon>int) \<le> 12"
    1.45 +value [nbe] "(10\<Colon>int) \<le> 12"
    1.46  
    1.47  value "max (2::int) 4"
    1.48 -value (code) "max (2::int) 4"
    1.49 -value (SML) "max (2::int) 4"
    1.50 -value ("normal_form") "max (2::int) 4"
    1.51 +value [code] "max (2::int) 4"
    1.52 +value [SML] "max (2::int) 4"
    1.53 +value [nbe] "max (2::int) 4"
    1.54  
    1.55  value "of_int 2 / of_int 4 * (1::rat)"
    1.56 -value (code) "of_int 2 / of_int 4 * (1::rat)"
    1.57 -value (SML) "of_int 2 / of_int 4 * (1::rat)"
    1.58 -value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"
    1.59 +value [code] "of_int 2 / of_int 4 * (1::rat)"
    1.60 +value [SML] "of_int 2 / of_int 4 * (1::rat)"
    1.61 +value [nbe] "of_int 2 / of_int 4 * (1::rat)"
    1.62  
    1.63  value "[]::nat list"
    1.64 -value (code) "[]::nat list"
    1.65 -value (SML) "[]::nat list"
    1.66 -value ("normal_form") "[]::nat list"
    1.67 +value [code] "[]::nat list"
    1.68 +value [SML] "[]::nat list"
    1.69 +value [nbe] "[]::nat list"
    1.70  
    1.71  value "[(nat 100, ())]"
    1.72 -value (code) "[(nat 100, ())]"
    1.73 -value (SML) "[(nat 100, ())]"
    1.74 -value ("normal_form") "[(nat 100, ())]"
    1.75 +value [code] "[(nat 100, ())]"
    1.76 +value [SML] "[(nat 100, ())]"
    1.77 +value [nbe] "[(nat 100, ())]"
    1.78  
    1.79  
    1.80  text {* a fancy datatype *}
    1.81 @@ -85,8 +85,8 @@
    1.82      Cair 'a 'b
    1.83  
    1.84  value "Shift (Cair (4::nat) [Suc 0])"
    1.85 -value (code) "Shift (Cair (4::nat) [Suc 0])"
    1.86 -value (SML) "Shift (Cair (4::nat) [Suc 0])"
    1.87 -value ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
    1.88 +value [code] "Shift (Cair (4::nat) [Suc 0])"
    1.89 +value [SML] "Shift (Cair (4::nat) [Suc 0])"
    1.90 +value [nbe] "Shift (Cair (4::nat) [Suc 0])"
    1.91  
    1.92  end