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.
Removed 'includes' (fixed).
authorballarin
Wed, 15 Oct 2008 16:06:59 +0200
changeset 28600 54352ed7114f
parent 28599 12d914277b8d
child 28601 b72589374396
Removed 'includes' (fixed).
src/HOL/Algebra/Divisibility.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle