type thm
STRUCTURE
SYNOPSIS
Type of theorems of the HOL logic.
DESCRIPTION
The abstract type thm represents the theorems derivable by inference in the HOL logic. The type of theorems can be viewed as the inductive closure of the axioms of the HOL logic by the primitive inference rules of HOL. Robin Milner had the brilliant insight to implement this view by encapsulating the primitive rules of inference for a logic as the constructors for an abstract type of theorems. This implementation technique is adopted in HOL.
SEEALSO
HOL  Kananaskis-14