thm

Thm.type thm

Type of theorems of the HOL logic.

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.

See also

Thm.dest_thm, Thm.hyp, Thm.concl, Thm.tag, Thm.ASSUME, Thm.REFL, Thm.BETA_CONV, Thm.ABS, Thm.DISCH, Thm.MP, Thm.SUBST, Thm.INST_TYPE