VERSION 2 (for HOL88.2.02) April 25, 2025

The HOL System

LIBRARIES

University of Cambridge  DSTO  SRI International

Preface

This volume provides documentation for the user-contributed libraries distributed with the HOL system. It should be read in conjunction with the HOL system documentation, which consists of three volumes:

(i) TUTORIAL: a tutorial introduction to HOL, with case studies.

(ii) DESCRIPTION: a description of higher order logic, the ML programming language, and theorem proving methods in the HOL system;

(iii) REFERENCE: the reference documentation of the tools available in HOL.

These documents are be referred to by the short names (in small slanted capitals) given above.

The present volume, LIBRARIES, contains a collection independent sections, one for each documented library distributed with the system. This documentation, which is written by the contributors of the corresponding HOL system libraries, is not, strictly speaking, part of the HOL manual set, which consists of the three volumes listed above. The LIBRARIES documentation is, however, typeset and distributed with the system in a form consistent with the HOL system documentation.