src/HOL/Algebra/Divisibility.thy

   ultimately
       show "p divides a \<or> p divides b" by fast
 qed
 
 
---"A version using @{const factors}, more complicated"
+\<comment>"A version using @{const factors}, more complicated"
 lemma (in factorial_monoid) factors_irreducible_is_prime:
   assumes pirr: "irreducible G p"
     and pcarr: "p \<in> carrier G"
   shows "prime G p"
 using pirr