src/HOL/Algebra/abstract/RingHomo.thy
changeset 17479 68a7acb5f22e
parent 13735 7de9342aca7a
child 20318 0e0ea63fe768
     1.1 --- a/src/HOL/Algebra/abstract/RingHomo.thy	Sat Sep 17 20:16:35 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/RingHomo.thy	Sat Sep 17 20:49:14 2005 +0200
     1.3 @@ -4,14 +4,12 @@
     1.4      Author: Clemens Ballarin, started 15 April 1997
     1.5  *)
     1.6  
     1.7 -RingHomo = Ring +
     1.8 -
     1.9 -consts
    1.10 -  homo	:: ('a::ring => 'b::ring) => bool
    1.11 +theory RingHomo imports Ring begin
    1.12  
    1.13 -defs
    1.14 -  homo_def	"homo f == (ALL a b. f (a + b) = f a + f b &
    1.15 -			      f (a * b) = f a * f b) &
    1.16 -			   f 1 = 1"
    1.17 +constdefs
    1.18 +  homo  :: "('a::ring => 'b::ring) => bool"
    1.19 +  "homo f == (ALL a b. f (a + b) = f a + f b &
    1.20 +                                   f (a * b) = f a * f b) &
    1.21 +                                   f 1 = 1"
    1.22  
    1.23  end