diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/Library/Code_Natural.thy --- a/src/HOL/Library/Code_Natural.thy Sat Mar 24 16:27:04 2012 +0100 +++ b/src/HOL/Library/Code_Natural.thy Sun Mar 25 20:15:39 2012 +0200 @@ -106,22 +106,26 @@ (Scala "Natural") setup {* - fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} + fold (Numeral.add_code @{const_name Code_Numeral.Num} false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"] *} code_instance code_numeral :: equal (Haskell -) -code_const "op + \ code_numeral \ code_numeral \ code_numeral" +code_const "0::code_numeral" + (Haskell "0") + (Scala "Natural(0)") + +code_const "plus \ code_numeral \ code_numeral \ code_numeral" (Haskell infixl 6 "+") (Scala infixl 7 "+") -code_const "op - \ code_numeral \ code_numeral \ code_numeral" +code_const "minus \ code_numeral \ code_numeral \ code_numeral" (Haskell infixl 6 "-") (Scala infixl 7 "-") -code_const "op * \ code_numeral \ code_numeral \ code_numeral" +code_const "times \ code_numeral \ code_numeral \ code_numeral" (Haskell infixl 7 "*") (Scala infixl 8 "*") @@ -133,11 +137,11 @@ (Haskell infix 4 "==") (Scala infixl 5 "==") -code_const "op \ \ code_numeral \ code_numeral \ bool" +code_const "less_eq \ code_numeral \ code_numeral \ bool" (Haskell infix 4 "<=") (Scala infixl 4 "<=") -code_const "op < \ code_numeral \ code_numeral \ bool" +code_const "less \ code_numeral \ code_numeral \ bool" (Haskell infix 4 "<") (Scala infixl 4 "<")