# HG changeset patch
# User haftmann
# Date 1277731944 -7200
# Node ID 501b0cae5aa806e5fd4dd17b01d09e3e23c94342
# Parent  2a4fb776ca53a6c393f049d0aafc665fe3b609f6
tuned whitespace

diff -r 2a4fb776ca53 -r 501b0cae5aa8 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Mon Jun 28 15:32:24 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Mon Jun 28 15:32:24 2010 +0200
@@ -1174,7 +1174,8 @@
   ultimately show ?case using prime_divprod[OF p] by blast
 qed
 
-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)
+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)
 
 (* Variant of Lucas theorem.                                                 *)