Cartan's theorems in HOL Light
------------------------------

Authors:
Gianni Ciolli
Graziano Gentili
Marco Maggesi


The present directory contains a computer checked formalization of
Cartan's rigidity theorem in the HOL Light theorem prover.

Read the file main.pdf for a brief introduction to this work.

This is a work in progress.  Some parts of the code are under revision
and some new theorems are being proved.

The main result archived so far is at the end of the file cartan.ml in
the present directory.