examples for evaluation oracle

--- a/src/HOL/ex/CodeEval.thy	Thu Jan 04 20:00:59 2007 +0100
+++ b/src/HOL/ex/CodeEval.thy	Thu Jan 04 20:01:00 2007 +0100
@@ -156,4 +156,9 @@
 
 ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
 
+text {* also test evaluation oracle *}
+
+lemma "True \<or> False" by eval
+lemma "\<not> (Suc 0 = Suc 1)" by eval
+
 end
\ No newline at end of file