[isabelle-dev] Multivariate analysis in Isabelle/HOL

[Amine Chaieb]

Dear all,

We are pleased to announce some progress in porting multivariate 
analysis from HOL Light. Several new theories are available now in the 
distribution from the definition of finite Cartesian products, to linear 
algebra on euclidean spaces, determinants, and topology on R^n. The 
latter formalizes several notions like convergence nets, cauchy 
sequences, completeness, compactness, continuity, Banach's and 
Edelstein's fixed point theorems. The theories have more than 13K lines 
of proofs and some 1K lines of SML code and are getting bigger and bigger.

So far we have been very pragmatic as to move on as fast as possible. 
This lead to the fact that some notions are not as general or as "nice" 
as one wishes them to be. Brian has already made some interesting 
comments and made some changes. Any further comments and suggestions are 
highly welcome!

Best wishes,

Robert Himmelmann and Amine Chaieb