dropped axclass
authorhaftmann
Tue Jul 24 15:20:48 2007 +0200 (2007-07-24)
changeset 23950f54c0e339061
parent 23949 06a988643235
child 23951 b188cac107ad
dropped axclass
src/HOL/IntDef.thy
     1.1 --- a/src/HOL/IntDef.thy	Tue Jul 24 15:20:47 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Tue Jul 24 15:20:48 2007 +0200
     1.3 @@ -428,9 +428,10 @@
     1.4  
     1.5  subsection{*Embedding of the Integers into any @{text ring_1}: @{term of_int}*}
     1.6  
     1.7 -constdefs
     1.8 -  of_int :: "int => 'a::ring_1"
     1.9 -  "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    1.10 +definition
    1.11 +  of_int :: "int \<Rightarrow> 'a\<Colon>ring_1"
    1.12 +where
    1.13 +  "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    1.14  lemmas [code func del] = of_int_def
    1.15  
    1.16  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
    1.17 @@ -486,7 +487,7 @@
    1.18  
    1.19  text{*Class for unital rings with characteristic zero.
    1.20   Includes non-ordered rings like the complex numbers.*}
    1.21 -axclass ring_char_0 < ring_1, semiring_char_0
    1.22 +class ring_char_0 = ring_1 + semiring_char_0
    1.23  
    1.24  lemma of_int_eq_iff [simp]:
    1.25       "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)"