--- 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