Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned whitespace
authorhaftmann
Mon, 28 Jun 2010 15:32:24 +0200
changeset 37602 501b0cae5aa8
parent 37601 2a4fb776ca53
child 37603 6e89e103f7c7
tuned whitespace
src/HOL/Old_Number_Theory/Pocklington.thy file | annotate | diff | comparison | revisions 
--- 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.                                                 *)
isabelle