HOL Light copyright notice, licence and disclaimer

                     (c) University of Cambridge 1998
                  (c) Copyright, John Harrison 1998-2008

HOL Light version 2.20, hereinafter referred to as "the software", is a
computer theorem proving system written by John Harrison. Much of the
software was developed at the University of Cambridge Computer Laboratory,
New Museums Site, Pembroke Street, Cambridge, CB2 3QG, England. The
software is copyright, University of Cambridge 1998 and John Harrison
1998-2007.

Permission to use, copy, modify, and distribute the software and its
documentation for any purpose and without fee is hereby granted. In the
case of further distribution of the software the present text, including
copyright notice, licence and disclaimer of warranty, must be included in
full and unmodified form in any release. Distribution of derivative
software obtained by modifying the software, or incorporating it into
other software, is permitted, provided the inclusion of the software is
acknowledged and that any changes made to the software are clearly
documented.

John Harrison and the University of Cambridge disclaim all warranties
with regard to the software, including all implied warranties of
merchantability and fitness. In no event shall John Harrison or the
University of Cambridge be liable for any special, indirect,
incidental or consequential damages or any damages whatsoever,
including, but not limited to, those arising from computer failure or
malfunction, work stoppage, loss of profit or loss of contracts.