--- a/src/HOL/ex/Eval_examples.thy Tue Jun 05 22:46:55 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Small examples for evaluation mechanisms *}
-
-theory Eval_examples
-imports Eval
-begin
-
-text {* evaluation oracle *}
-
-lemma "True \<or> False" by eval
-lemma "\<not> (Suc 0 = Suc 1)" by eval
-
-text {* term evaluation *}
-
-value (overloaded) "(Suc 2 + 1) * 4"
-value (overloaded) "(Suc 2 + 1) * 4"
-value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
-value (overloaded) "[]::nat list"
-value (overloaded) "fst ([]::nat list, Suc 0) = []"
-value (overloaded) "nat 100"
-value (overloaded) "[(nat 100, ())]"
-value (overloaded) "int 10 \<le> 12"
-
-text {* a fancy datatype *}
-
-datatype ('a, 'b) bair =
- Bair "'a\<Colon>order" 'b
- | Shift "('a, 'b) cair"
- | Dummy unit
-and ('a, 'b) cair =
- Cair 'a 'b
-
-value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
-
-end
\ No newline at end of file