thm Type

Namespace: HOL
Assembly: nholz.dll
Parent Module: Thm
Base Type: obj
All Interfaces: IEquatable<thm> , IStructuralEquatable , IComparable<thm> , IComparable , IStructuralComparable

This is the datatype for internal HOL theorems. A theorem consists of a list of assumptions and a conclusion, all of which are boolean terms.