# HG changeset patch
# User haftmann
# Date 1192803479 -7200
# Node ID b2c19b9964db1ab399a7731e1226b0195db041c4
# Parent  1ec53c9ae71a8b2d6c34cab0445bec6c6cb9cd03
lemmas with normalization

diff -r 1ec53c9ae71a -r b2c19b9964db src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Fri Oct 19 16:13:55 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Fri Oct 19 16:17:59 2007 +0200
@@ -8,6 +8,14 @@
 imports Eval "~~/src/HOL/Real/Rational"
 begin
 
+text {* evaluation oracle *}
+
+lemma "True \<or> False" by eval
+lemma "\<not> (Suc 0 = Suc 1)" by eval
+lemma "[] = ([]\<Colon> int list)" by eval
+lemma "[()] = [()]" by eval
+lemma "fst ([]::nat list, Suc 0) = []" by eval
+
 text {* SML evaluation oracle *}
 
 lemma "True \<or> False" by evaluation
@@ -16,13 +24,13 @@
 lemma "[()] = [()]" by evaluation
 lemma "fst ([]::nat list, Suc 0) = []" by evaluation
 
-text {* evaluation oracle *}
+text {* normalization *}
 
-lemma "True \<or> False" by eval
-lemma "\<not> (Suc 0 = Suc 1)" by eval
-lemma "[] = ([]\<Colon> int list)" by eval
-lemma "[()] = [()]" by eval
-lemma "fst ([]::nat list, Suc 0) = []" by eval
+lemma "True \<or> False" by normalization
+lemma "\<not> (Suc 0 = Suc 1)" by normalization
+lemma "[] = ([]\<Colon> int list)" by normalization
+lemma "[()] = [()]" by normalization
+lemma "fst ([]::nat list, Suc 0) = []" by normalization
 
 text {* term evaluation *}
 
@@ -58,12 +66,12 @@
 
 value "[]::nat list"
 value (code) "[]::nat list"
-(*value (SML) "[]::nat list" FIXME*)
+value (SML) "[]::nat list"
 value ("normal_form") "[]::nat list"
 
 value "[(nat 100, ())]"
 value (code) "[(nat 100, ())]"
-(*value (SML) "[(nat 100, ())]" FIXME*)
+value (SML) "[(nat 100, ())]"
 value ("normal_form") "[(nat 100, ())]"