Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Eval_Examples.thy
changeset 28227 77221ee0f7b9
parent 26020 ffe1a032d24b
child 28952 15a4b2cf8c34 
--- a/src/HOL/ex/Eval_Examples.thy	Mon Sep 15 20:51:58 2008 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Tue Sep 16 09:21:22 2008 +0200
@@ -5,7 +5,7 @@
 header {* Small examples for evaluation mechanisms *}
 
 theory Eval_Examples
-imports Eval "~~/src/HOL/Real/Rational"
+imports Code_Eval "~~/src/HOL/Real/Rational"
 begin
 
 text {* evaluation oracle *}
@@ -35,44 +35,44 @@
 text {* term evaluation *}
 
 value "(Suc 2 + 1) * 4"
-value (code) "(Suc 2 + 1) * 4"
-value (SML) "(Suc 2 + 1) * 4"
-value ("normal_form") "(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 ("normal_form") "(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 ("normal_form") "nat 100"
+value [code] "nat 100"
+value [SML] "nat 100"
+value [nbe] "nat 100"
 
 value "(10\<Colon>int) \<le> 12"
-value (code) "(10\<Colon>int) \<le> 12"
-value (SML) "(10\<Colon>int) \<le> 12"
-value ("normal_form") "(10\<Colon>int) \<le> 12"
+value [code] "(10\<Colon>int) \<le> 12"
+value [SML] "(10\<Colon>int) \<le> 12"
+value [nbe] "(10\<Colon>int) \<le> 12"
 
 value "max (2::int) 4"
-value (code) "max (2::int) 4"
-value (SML) "max (2::int) 4"
-value ("normal_form") "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 ("normal_form") "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 ("normal_form") "[]::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 ("normal_form") "[(nat 100, ())]"
+value [code] "[(nat 100, ())]"
+value [SML] "[(nat 100, ())]"
+value [nbe] "[(nat 100, ())]"
 
 
 text {* a fancy datatype *}
@@ -85,8 +85,8 @@
     Cair 'a 'b
 
 value "Shift (Cair (4::nat) [Suc 0])"
-value (code) "Shift (Cair (4::nat) [Suc 0])"
-value (SML) "Shift (Cair (4::nat) [Suc 0])"
-value ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
+value [code] "Shift (Cair (4::nat) [Suc 0])"
+value [SML] "Shift (Cair (4::nat) [Suc 0])"
+value [nbe] "Shift (Cair (4::nat) [Suc 0])"
 
 end
isabelle