# HG changeset patch
# User haftmann
# Date 1167937260 -3600
# Node ID 0faa5afd5d69e880c7dea856a9f3d78f0d05a147
# Parent  a69d21fc6d68a89076cebd0ee7979cb762ab9c7f
examples for evaluation oracle

diff -r a69d21fc6d68 -r 0faa5afd5d69 src/HOL/ex/CodeEval.thy
--- 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