1.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Mon Jun 28 15:32:24 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Mon Jun 28 15:32:24 2010 +0200
     1.3 @@ -1174,7 +1174,8 @@
     1.4    ultimately show ?case using prime_divprod[OF p] by blast
     1.5  qed
     1.6  
     1.7 -lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps" by (auto simp add: primefact_def list_all_iff)
     1.8 +lemma primefact_variant: "primefact ps n \<longleftrightarrow> foldr op * ps 1 = n \<and> list_all prime ps"
     1.9 +  by (auto simp add: primefact_def list_all_iff)
    1.10  
    1.11  (* Variant of Lucas theorem.                                                 *)
    1.12