1.1 --- a/src/HOL/ex/Eval_Examples.thy	Fri Nov 26 23:50:14 2010 +0100
     1.2 +++ b/src/HOL/ex/Eval_Examples.thy	Sat Nov 27 19:41:27 2010 +0100
     1.3 @@ -9,26 +9,26 @@
     1.4  text {* evaluation oracle *}
     1.5  
     1.6  lemma "True \<or> False" by eval
     1.7 -lemma "\<not> (Suc 0 = Suc 1)" by eval
     1.8 -lemma "[] = ([]\<Colon> int list)" by eval
     1.9 +lemma "Suc 0 \<noteq> Suc 1" by eval
    1.10 +lemma "[] = ([] :: int list)" by eval
    1.11  lemma "[()] = [()]" by eval
    1.12 -lemma "fst ([]::nat list, Suc 0) = []" by eval
    1.13 +lemma "fst ([] :: nat list, Suc 0) = []" by eval
    1.14  
    1.15  text {* SML evaluation oracle *}
    1.16  
    1.17  lemma "True \<or> False" by evaluation
    1.18 -lemma "\<not> (Suc 0 = Suc 1)" by evaluation
    1.19 -lemma "[] = ([]\<Colon> int list)" by evaluation
    1.20 +lemma "Suc 0 \<noteq> Suc 1" by evaluation
    1.21 +lemma "[] = ([] :: int list)" by evaluation
    1.22  lemma "[()] = [()]" by evaluation
    1.23 -lemma "fst ([]::nat list, Suc 0) = []" by evaluation
    1.24 +lemma "fst ([] :: nat list, Suc 0) = []" by evaluation
    1.25  
    1.26  text {* normalization *}
    1.27  
    1.28  lemma "True \<or> False" by normalization
    1.29 -lemma "\<not> (Suc 0 = Suc 1)" by normalization
    1.30 -lemma "[] = ([]\<Colon> int list)" by normalization
    1.31 +lemma "Suc 0 \<noteq> Suc 1" by normalization
    1.32 +lemma "[] = ([] :: int list)" by normalization
    1.33  lemma "[()] = [()]" by normalization
    1.34 -lemma "fst ([]::nat list, Suc 0) = []" by normalization
    1.35 +lemma "fst ([] :: nat list, Suc 0) = []" by normalization
    1.36  
    1.37  text {* term evaluation *}
    1.38  
    1.39 @@ -47,10 +47,10 @@
    1.40  value [SML] "nat 100"
    1.41  value [nbe] "nat 100"
    1.42  
    1.43 -value "(10\<Colon>int) \<le> 12"
    1.44 -value [code] "(10\<Colon>int) \<le> 12"
    1.45 -value [SML] "(10\<Colon>int) \<le> 12"
    1.46 -value [nbe] "(10\<Colon>int) \<le> 12"
    1.47 +value "(10::int) \<le> 12"
    1.48 +value [code] "(10::int) \<le> 12"
    1.49 +value [SML] "(10::int) \<le> 12"
    1.50 +value [nbe] "(10::int) \<le> 12"
    1.51  
    1.52  value "max (2::int) 4"
    1.53  value [code] "max (2::int) 4"
    1.54 @@ -62,17 +62,16 @@
    1.55  value [SML] "of_int 2 / of_int 4 * (1::rat)"
    1.56  value [nbe] "of_int 2 / of_int 4 * (1::rat)"
    1.57  
    1.58 -value "[]::nat list"
    1.59 -value [code] "[]::nat list"
    1.60 -value [SML] "[]::nat list"
    1.61 -value [nbe] "[]::nat list"
    1.62 +value "[] :: nat list"
    1.63 +value [code] "[] :: nat list"
    1.64 +value [SML] "[] :: nat list"
    1.65 +value [nbe] "[] :: nat list"
    1.66  
    1.67  value "[(nat 100, ())]"
    1.68  value [code] "[(nat 100, ())]"
    1.69  value [SML] "[(nat 100, ())]"
    1.70  value [nbe] "[(nat 100, ())]"
    1.71  
    1.72 -
    1.73  text {* a fancy datatype *}
    1.74  
    1.75  datatype ('a, 'b) foo =