src/HOL/Algebra/abstract/Factor.ML
changeset 17479 68a7acb5f22e
parent 13735 7de9342aca7a
child 21416 f23e4e75dfd3
     1.1 --- a/src/HOL/Algebra/abstract/Factor.ML	Sat Sep 17 20:16:35 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Factor.ML	Sat Sep 17 20:49:14 2005 +0200
     1.3 @@ -33,14 +33,14 @@
     1.4  by (Auto_tac);
     1.5  qed "irred_dvd_list";
     1.6  
     1.7 -Goalw [Factorisation_def] "!! c::'a::factorial. \
     1.8 +Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \
     1.9  \  [| irred c; Factorisation x factors u; c dvd x |] ==> \
    1.10  \  EX d. c assoc d & d : set factors";
    1.11  by (rtac (irred_dvd_list_lemma RS mp) 1);
    1.12  by (Auto_tac);
    1.13  qed "Factorisation_dvd";
    1.14  
    1.15 -Goalw [Factorisation_def] "!! c::'a::factorial. \
    1.16 +Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \
    1.17  \  [| Factorisation x factors u; a : set factors |] ==> irred a";
    1.18  by (Blast_tac 1);
    1.19  qed "Factorisation_irred";