==== this is no question and no opening for discussion - just for your interest ===
Dear all, This afternoon, I defined the following class class acf = field + assumes algebraically_closed: "~ constant (poly p) ==> EX x. poly p x = 0" and the following proof: instance complex :: acf using fundamental_theorem_of_algebra by (intro_classes, blast) This would have not been possible without merging some classes. There is a quantifier elimination procedure implemented for complex numbers, which relies on fact easily portable to acf. There is great future in merging classes, so why not roar ahead? Amine.