tuned

--- a/src/HOL/ex/Eval_Examples.thy	Fri Nov 26 23:50:14 2010 +0100
+++ b/src/HOL/ex/Eval_Examples.thy	Sat Nov 27 19:41:27 2010 +0100
@@ -9,26 +9,26 @@
 text {* evaluation oracle *}
 
 lemma "True \<or> False" by eval
-lemma "\<not> (Suc 0 = Suc 1)" by eval
-lemma "[] = ([]\<Colon> int list)" by eval
+lemma "Suc 0 \<noteq> Suc 1" by eval
+lemma "[] = ([] :: int list)" by eval
 lemma "[()] = [()]" by eval
-lemma "fst ([]::nat list, Suc 0) = []" by eval
+lemma "fst ([] :: nat list, Suc 0) = []" by eval
 
 text {* SML evaluation oracle *}
 
 lemma "True \<or> False" by evaluation
-lemma "\<not> (Suc 0 = Suc 1)" by evaluation
-lemma "[] = ([]\<Colon> int list)" by evaluation
+lemma "Suc 0 \<noteq> Suc 1" by evaluation
+lemma "[] = ([] :: int list)" by evaluation
 lemma "[()] = [()]" by evaluation
-lemma "fst ([]::nat list, Suc 0) = []" by evaluation
+lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
 
 text {* normalization *}
 
 lemma "True \<or> False" by normalization
-lemma "\<not> (Suc 0 = Suc 1)" by normalization
-lemma "[] = ([]\<Colon> int list)" by normalization
+lemma "Suc 0 \<noteq> Suc 1" by normalization
+lemma "[] = ([] :: int list)" by normalization
 lemma "[()] = [()]" by normalization
-lemma "fst ([]::nat list, Suc 0) = []" by normalization
+lemma "fst ([] :: nat list, Suc 0) = []" by normalization
 
 text {* term evaluation *}
 
@@ -47,10 +47,10 @@
 value [SML] "nat 100"
 value [nbe] "nat 100"
 
-value "(10\<Colon>int) \<le> 12"
-value [code] "(10\<Colon>int) \<le> 12"
-value [SML] "(10\<Colon>int) \<le> 12"
-value [nbe] "(10\<Colon>int) \<le> 12"
+value "(10::int) \<le> 12"
+value [code] "(10::int) \<le> 12"
+value [SML] "(10::int) \<le> 12"
+value [nbe] "(10::int) \<le> 12"
 
 value "max (2::int) 4"
 value [code] "max (2::int) 4"
@@ -62,17 +62,16 @@
 value [SML] "of_int 2 / of_int 4 * (1::rat)"
 value [nbe] "of_int 2 / of_int 4 * (1::rat)"
 
-value "[]::nat list"
-value [code] "[]::nat list"
-value [SML] "[]::nat list"
-value [nbe] "[]::nat list"
+value "[] :: nat list"
+value [code] "[] :: nat list"
+value [SML] "[] :: nat list"
+value [nbe] "[] :: nat list"
 
 value "[(nat 100, ())]"
 value [code] "[(nat 100, ())]"
 value [SML] "[(nat 100, ())]"
 value [nbe] "[(nat 100, ())]"
 
-
 text {* a fancy datatype *}
 
 datatype ('a, 'b) foo =