==================================================
THE FORMALISATION OF THE REFOCUSING TRANSFORMATION
by Filip Sieczkowski, University of Wrocław
July 2010
==================================================

The source can be compiled using 'make'. It is known to compile correctly using
Coq 8.2pl1.

Each part of the formalisation depends on the utils/Util module.
The dependencies inside each part of the formalisation are as follows:
1. refocusing_lang
2. refocusing_signatures
3. refocusing_substitutions (or refocusing_environments)
4. case studies