# HG changeset patch
# User huffman
# Date 1187632372 -7200
# Node ID 93d78fdeb55a99bce5aa9d865de134473f1d0823
# Parent  0fdabe28f0e6e1d27c9ea8c853f2da890ce425cd
remove int_of_nat

diff -r 0fdabe28f0e6 -r 93d78fdeb55a src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Mon Aug 20 19:52:24 2007 +0200
+++ b/src/HOL/IntDef.thy	Mon Aug 20 19:52:52 2007 +0200
@@ -682,9 +682,4 @@
 where
   "int \<equiv> of_nat"
 
-abbreviation
-  int_of_nat :: "nat \<Rightarrow> int"
-where
-  "int_of_nat \<equiv> of_nat"
-
 end
diff -r 0fdabe28f0e6 -r 93d78fdeb55a src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Mon Aug 20 19:52:24 2007 +0200
+++ b/src/HOL/Real/RComplete.thy	Mon Aug 20 19:52:52 2007 +0200
@@ -480,7 +480,7 @@
 lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0"
 by auto
 
-lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int_of_nat n"
+lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n"
 apply (simp only: floor_def)
 apply (rule Least_equality)
 apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
@@ -488,7 +488,7 @@
 apply simp_all
 done
 
-lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int_of_nat n"
+lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n"
 apply (simp only: floor_def)
 apply (rule Least_equality)
 apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst])
@@ -753,7 +753,7 @@
 lemma ceiling_zero [simp]: "ceiling 0 = 0"
 by (simp add: ceiling_def)
 
-lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int_of_nat n"
+lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
 by (simp add: ceiling_def)
 
 lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0"
@@ -1043,7 +1043,7 @@
 
 lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
   apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int_of_nat a)")
+  apply (subgoal_tac "real a = real (int a)")
   apply (erule ssubst)
   apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq)
   apply simp
@@ -1065,7 +1065,7 @@
 lemma natfloor_subtract [simp]: "real a <= x ==>
     natfloor(x - real a) = natfloor x - a"
   apply (unfold natfloor_def)
-  apply (subgoal_tac "real a = real (int_of_nat a)")
+  apply (subgoal_tac "real a = real (int a)")
   apply (erule ssubst)
   apply (simp del: real_of_int_of_nat_eq)
   apply simp
@@ -1176,7 +1176,7 @@
 lemma natceiling_add [simp]: "0 <= x ==>
     natceiling (x + real a) = natceiling x + a"
   apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int_of_nat a)")
+  apply (subgoal_tac "real a = real (int a)")
   apply (erule ssubst)
   apply (simp del: real_of_int_of_nat_eq)
   apply (subst nat_add_distrib)
@@ -1202,7 +1202,7 @@
 lemma natceiling_subtract [simp]: "real a <= x ==>
     natceiling(x - real a) = natceiling x - a"
   apply (unfold natceiling_def)
-  apply (subgoal_tac "real a = real (int_of_nat a)")
+  apply (subgoal_tac "real a = real (int a)")
   apply (erule ssubst)
   apply (simp del: real_of_int_of_nat_eq)
   apply simp