equal
deleted
inserted
replaced
894 |
894 |
895 lemma mod_divmod [code]: |
895 lemma mod_divmod [code]: |
896 "m mod n = snd (divmod m n)" |
896 "m mod n = snd (divmod m n)" |
897 unfolding divmod_def by simp |
897 unfolding divmod_def by simp |
898 |
898 |
899 code_constname |
899 code_modulename SML |
900 "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.div_nat" |
900 Divides Integer |
901 "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.mod_nat" |
|
902 Divides.divmod "IntDef.divmod_nat" |
|
903 |
901 |
904 hide (open) const divmod |
902 hide (open) const divmod |
905 |
903 |
906 |
904 |
907 subsection {* Legacy bindings *} |
905 subsection {* Legacy bindings *} |