[isabelle-dev] classes

Amine Chaieb 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 
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?


More information about the isabelle-dev mailing list