src/HOL/Algebra/abstract/RingHomo.thy
changeset 13735 7de9342aca7a
parent 7998 3d0c34795831
child 17479 68a7acb5f22e
     1.1 --- a/src/HOL/Algebra/abstract/RingHomo.thy	Wed Nov 27 17:25:41 2002 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/RingHomo.thy	Thu Nov 28 10:50:42 2002 +0100
     1.3 @@ -4,14 +4,14 @@
     1.4      Author: Clemens Ballarin, started 15 April 1997
     1.5  *)
     1.6  
     1.7 -RingHomo = NatSum +
     1.8 +RingHomo = Ring +
     1.9  
    1.10  consts
    1.11 -  homo	:: ('a::ringS => 'b::ringS) => bool
    1.12 +  homo	:: ('a::ring => 'b::ring) => bool
    1.13  
    1.14  defs
    1.15    homo_def	"homo f == (ALL a b. f (a + b) = f a + f b &
    1.16  			      f (a * b) = f a * f b) &
    1.17 -			   f <1> = <1>"
    1.18 +			   f 1 = 1"
    1.19  
    1.20  end