--- a/src/HOL/Divides.thy Wed Sep 20 12:23:54 2006 +0200
+++ b/src/HOL/Divides.thy Wed Sep 20 12:24:11 2006 +0200
@@ -896,6 +896,11 @@
"m mod n = snd (divmod m n)"
unfolding divmod_def by simp
+code_constname
+ "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.div_nat"
+ "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.mod_nat"
+ Divides.divmod "IntDef.divmod_nat"
+
hide (open) const divmod
--- a/src/HOL/Nat.thy Wed Sep 20 12:23:54 2006 +0200
+++ b/src/HOL/Nat.thy Wed Sep 20 12:24:11 2006 +0200
@@ -1062,4 +1062,18 @@
lemma [code func]:
"OperationalEquality.eq 0 (Suc m) = False" unfolding eq_def by auto
+code_typename
+ "nat" "IntDef.nat"
+
+code_constname
+ "0 \<Colon> nat" "IntDef.zero_nat"
+ "1 \<Colon> nat" "IntDef.one_nat"
+ Suc "IntDef.succ_nat"
+ "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.plus_nat"
+ "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.minus_nat"
+ "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.times_nat"
+ "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_nat"
+ "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_eq_nat"
+ "OperationalEquality.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.eq_nat"
+
end