| author | paulson |
| Fri, 05 Nov 1999 11:14:26 +0100 | |
| changeset 7998 | 3d0c34795831 |
| child 13735 | 7de9342aca7a |
| permissions | -rw-r--r-- |
| paulson@7998 | 1 |
(* |
| paulson@7998 | 2 |
Ring homomorphism |
| paulson@7998 | 3 |
$Id$ |
| paulson@7998 | 4 |
Author: Clemens Ballarin, started 15 April 1997 |
| paulson@7998 | 5 |
*) |
| paulson@7998 | 6 |
|
| paulson@7998 | 7 |
RingHomo = NatSum + |
| paulson@7998 | 8 |
|
| paulson@7998 | 9 |
consts |
| paulson@7998 | 10 |
homo :: ('a::ringS => 'b::ringS) => bool
|
| paulson@7998 | 11 |
|
| paulson@7998 | 12 |
defs |
| paulson@7998 | 13 |
homo_def "homo f == (ALL a b. f (a + b) = f a + f b & |
| paulson@7998 | 14 |
f (a * b) = f a * f b) & |
| paulson@7998 | 15 |
f <1> = <1>" |
| paulson@7998 | 16 |
|
| paulson@7998 | 17 |
end |