diff -r 4baa475a51e6 -r 7dd207fe7b6e src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Wed Oct 19 08:37:14 2011 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Wed Oct 19 08:37:15 2011 +0200
@@ -14,14 +14,6 @@
 lemma "[()] = [()]" by eval
 lemma "fst ([] :: nat list, Suc 0) = []" by eval
 
-text {* SML evaluation oracle *}
-
-lemma "True \<or> False" by evaluation
-lemma "Suc 0 \<noteq> Suc 1" by evaluation
-lemma "[] = ([] :: int list)" by evaluation
-lemma "[()] = [()]" by evaluation
-lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
-
 text {* normalization *}
 
 lemma "True \<or> False" by normalization