chaieb at in.tum.de
Wed Nov 7 19:33:22 CET 2007
==== this is no question and no opening for discussion - just for your
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?
More information about the isabelle-dev