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