summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Algebra/Divisibility.thy

changeset 28600 | 54352ed7114f |

parent 28599 | 12d914277b8d |

child 28823 | dcbef866c9e2 |

--- a/src/HOL/Algebra/Divisibility.thy Wed Oct 15 15:44:15 2008 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Wed Oct 15 16:06:59 2008 +0200 @@ -1344,7 +1344,6 @@ by (fast dest: e) lemma (in monoid) factorsI: - fixes G (structure) assumes "\<forall>f\<in>set fs. irreducible G f" and "foldr (op \<otimes>) fs \<one> = a" shows "factors G fs a"