Filter
Top Products
Legal notice
HOL Light version 1.0, hereinafter referred to as “the software”, is a
computer theorem proving system written by John Harrison, a research
worker at the University of Cambridge Computer Laboratory, New Mu-
seums Site, Pembroke Street, Cambridge, CB2 3QG, England. The soft-
ware is copyright,
c
University of Cambridge 1998.
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 war-
ranties 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.
i