--- a/src/HOL/Algebra/abstract/RingHomo.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/RingHomo.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,14 +4,12 @@
Author: Clemens Ballarin, started 15 April 1997
*)
-RingHomo = Ring +
-
-consts
- homo :: ('a::ring => 'b::ring) => bool
+theory RingHomo imports Ring begin
-defs
- homo_def "homo f == (ALL a b. f (a + b) = f a + f b &
- f (a * b) = f a * f b) &
- f 1 = 1"
+constdefs
+ homo :: "('a::ring => 'b::ring) => bool"
+ "homo f == (ALL a b. f (a + b) = f a + f b &
+ f (a * b) = f a * f b) &
+ f 1 = 1"
end