[isabelle] Is factorization mechanization for any kind of algebra?



Hi 
http://isabelle.in.tum.de/website-Isabelle2011/dist/library/HOL/Old_Number_Theory/Factorization.html
is it possible to do factorization mechanization for any kind of algebra?
such as semigroup, lattice, operator algebra etc.
is it possible to mechanize of construction of basis with this factorization for any kind of algebra?
Regards,
Martin 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.