--- 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