1
(*
2
Ring homomorphism
3
$Id$
4
Author: Clemens Ballarin, started 15 April 1997
5
*)
6
7
RingHomo = NatSum +
8
9
consts
10
homo :: ('a::ringS => 'b::ringS) => bool
11
12
defs
13
homo_def "homo f == (ALL a b. f (a + b) = f a + f b &
14
f (a * b) = f a * f b) &
15
f <1> = <1>"
16
17
end