| changeset 22005 | 0faa5afd5d69 |
| parent 21924 | fe474e69e603 |
| child 22017 | 9b1656a28c88 |
--- 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