equal
deleted
inserted
replaced
940 (Haskell infixl 7 "*") |
940 (Haskell infixl 7 "*") |
941 |
941 |
942 code_const "uminus \<Colon> int \<Rightarrow> int" |
942 code_const "uminus \<Colon> int \<Rightarrow> int" |
943 (SML target_atom "IntInf.~") |
943 (SML target_atom "IntInf.~") |
944 (Haskell target_atom "negate") |
944 (Haskell target_atom "negate") |
|
945 |
|
946 code_reserved SML IntInf |
|
947 code_reserved Haskell Integer negate |
945 |
948 |
946 ML {* |
949 ML {* |
947 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", |
950 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", |
948 Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = |
951 Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = |
949 (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), |
952 (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), |