# HG changeset patch
# User haftmann
# Date 1185283248 -7200
# Node ID f54c0e339061c8611357ea2402b0c310a7196795
# Parent  06a988643235390e17c127117e6ca08908ce586e
dropped axclass

diff -r 06a988643235 -r f54c0e339061 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Tue Jul 24 15:20:47 2007 +0200
+++ b/src/HOL/IntDef.thy	Tue Jul 24 15:20:48 2007 +0200
@@ -428,9 +428,10 @@
 
 subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
 
-constdefs
-  of_int :: "int => 'a::ring_1"
-  "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+definition
+  of_int :: "int \<Rightarrow> 'a\<Colon>ring_1"
+where
+  "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 lemmas [code func del] = of_int_def
 
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
@@ -486,7 +487,7 @@
 
 text{*Class for unital rings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
-axclass ring_char_0 < ring_1, semiring_char_0
+class ring_char_0 = ring_1 + semiring_char_0
 
 lemma of_int_eq_iff [simp]:
      "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"