[isabelle-dev] classes

[Amine Chaieb]

==== 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.