Package relation-measure-def: relation-measure-def

Information

namerelation-measure-def
version1.8
descriptionrelation-measure-def
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-18
showData.Bool

Files

Defined Constant

Theorem

m. Relation.measure m = λx y. Number.Natural.< (m x) (m y)

Input Type Operators

Input Constants

Assumptions

T

() = λp. p = λx. T