1.1 --- a/src/HOL/Library/Code_Natural.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -106,22 +106,26 @@
     1.4    (Scala "Natural")
     1.5  
     1.6  setup {*
     1.7 -  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
     1.8 +  fold (Numeral.add_code @{const_name Code_Numeral.Num}
     1.9      false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
    1.10  *}
    1.11  
    1.12  code_instance code_numeral :: equal
    1.13    (Haskell -)
    1.14  
    1.15 -code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.16 +code_const "0::code_numeral"
    1.17 +  (Haskell "0")
    1.18 +  (Scala "Natural(0)")
    1.19 +
    1.20 +code_const "plus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.21    (Haskell infixl 6 "+")
    1.22    (Scala infixl 7 "+")
    1.23  
    1.24 -code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.25 +code_const "minus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.26    (Haskell infixl 6 "-")
    1.27    (Scala infixl 7 "-")
    1.28  
    1.29 -code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.30 +code_const "times \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.31    (Haskell infixl 7 "*")
    1.32    (Scala infixl 8 "*")
    1.33  
    1.34 @@ -133,11 +137,11 @@
    1.35    (Haskell infix 4 "==")
    1.36    (Scala infixl 5 "==")
    1.37  
    1.38 -code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.39 +code_const "less_eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.40    (Haskell infix 4 "<=")
    1.41    (Scala infixl 4 "<=")
    1.42  
    1.43 -code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.44 +code_const "less \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.45    (Haskell infix 4 "<")
    1.46    (Scala infixl 4 "<")
    1.47