Package bool-def: Boolean definitions

Information

namebool-def
version1.8
descriptionBoolean definitions
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-12-18
showData.Bool

Files

Defined Constants

Theorems

F p. p

(¬) = λp. p F

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

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

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f T T

() = λp. q. (x. p x q) q

() = λp q. r. (p r) (q r) r

(∃!) = λp. () p x y. p x p y x = y

cond = λt t1 t2. select x. ((t T) x = t1) ((t F) x = t2)

Input Type Operators

Input Constants