# HG changeset patch
# User haftmann
# Date 1187257505 -7200
# Node ID 26ac9fe0e80ead36aa9fa7b1ef5595c84b230cde
# Parent  fa72aab966dca6c3c022d57a5d0e7a1af34f4f50
added evaluation examples

diff -r fa72aab966dc -r 26ac9fe0e80e src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Wed Aug 15 22:21:13 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Thu Aug 16 11:45:05 2007 +0200
@@ -8,12 +8,21 @@
 imports Eval
 begin
 
+text {* SML evaluation oracle *}
+
+lemma "True \<or> False" by evaluation
+lemma "\<not> (Suc 0 = Suc 1)" by evaluation
+lemma "[] = ([]\<Colon> int list)" by evaluation
+lemma "[()] = [()]" by evaluation
+lemma "fst ([]::nat list, Suc 0) = []" by evaluation
+
 text {* evaluation oracle *}
 
 lemma "True \<or> False" by eval
 lemma "\<not> (Suc 0 = Suc 1)" by eval
 lemma "[] = ([]\<Colon> int list)" by eval
 lemma "[()] = [()]" by eval
+lemma "fst ([]::nat list, Suc 0) = []" by eval
 
 text {* term evaluation *}
 
@@ -24,7 +33,6 @@
 value (overloaded) "(10\<Colon>int) \<le> 12"
 value (overloaded) "[(nat 100, ())]"
 value (overloaded) "[]::nat list"
-value (overloaded) "fst ([]::nat list, Suc 0) = []"
 
 text {* a fancy datatype *}
 
diff -r fa72aab966dc -r 26ac9fe0e80e src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Aug 15 22:21:13 2007 +0200
+++ b/src/Tools/nbe.ML	Thu Aug 16 11:45:05 2007 +0200
@@ -346,7 +346,7 @@
   Logic.mk_equals (t, eval thy code t t' deps);
 
 fun normalization_invoke thy code t t' deps =
-  Thm.invoke_oracle_i thy "Code_Setup.normalization" (thy, Normalization (code, t, t', deps));
+  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t', deps));
   (*FIXME get rid of hardwired theory name*)
 
 fun normalization_conv ct =