equal
deleted
inserted
replaced
927 lemma [code inline]: |
927 lemma [code inline]: |
928 "op dvd = dvd_nat" |
928 "op dvd = dvd_nat" |
929 by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq) |
929 by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq) |
930 |
930 |
931 code_modulename SML |
931 code_modulename SML |
932 Divides Integer |
932 Divides Nat |
933 |
933 |
934 code_modulename OCaml |
934 code_modulename OCaml |
935 Divides Integer |
935 Divides Nat |
|
936 |
|
937 code_modulename Haskell |
|
938 Divides Nat |
936 |
939 |
937 hide (open) const divmod dvd_nat |
940 hide (open) const divmod dvd_nat |
938 |
941 |
939 subsection {* Legacy bindings *} |
942 subsection {* Legacy bindings *} |
940 |
943 |