src/HOL/Algebra/abstract/RingHomo.thy

moved bires_inst_tac etc. to rule_insts.ML;

(*
    Ring homomorphism
    $Id$
    Author: Clemens Ballarin, started 15 April 1997
*)

theory RingHomo imports Ring2 begin

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