src/HOL/Algebra/abstract/RingHomo.ML
changeset 17479 68a7acb5f22e
parent 13783 3294f727e20d
     1.1 --- a/src/HOL/Algebra/abstract/RingHomo.ML	Sat Sep 17 20:16:35 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/RingHomo.ML	Sat Sep 17 20:49:14 2005 +0200
     1.3 @@ -6,21 +6,21 @@
     1.4  
     1.5  (* Ring homomorphism *)
     1.6  
     1.7 -Goalw [homo_def]
     1.8 +Goalw [thm "homo_def"]
     1.9    "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \
    1.10  \           f 1 = 1 |] ==> homo f";
    1.11  by Auto_tac;
    1.12  qed "homoI";
    1.13  
    1.14 -Goalw [homo_def] "!! f. homo f ==> f (a + b) = f a + f b";
    1.15 +Goalw [thm "homo_def"] "!! f. homo f ==> f (a + b) = f a + f b";
    1.16  by (Fast_tac 1);
    1.17  qed "homo_add";
    1.18  
    1.19 -Goalw [homo_def] "!! f. homo f ==> f (a * b) = f a * f b";
    1.20 +Goalw [thm "homo_def"] "!! f. homo f ==> f (a * b) = f a * f b";
    1.21  by (Fast_tac 1);
    1.22  qed "homo_mult";
    1.23  
    1.24 -Goalw [homo_def] "!! f. homo f ==> f 1 = 1";
    1.25 +Goalw [thm "homo_def"] "!! f. homo f ==> f 1 = 1";
    1.26  by (Fast_tac 1);
    1.27  qed "homo_one";
    1.28