# HG changeset patch
# User haftmann
# Date 1158747851 -7200
# Node ID 05e6042394b91da51a3f4881f3600c46bbdaf41f
# Parent  3aa960295c545f91c8318cb3ebc7fbbd3b3da2ed
name shifts

diff -r 3aa960295c54 -r 05e6042394b9 src/HOL/Divides.thy
--- 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
 
 
diff -r 3aa960295c54 -r 05e6042394b9 src/HOL/Nat.thy
--- 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