Package bool-def-or: bool-def-or
Information
name
bool-def-or
version
1.0
description
bool-def-or
author
Joe Hurd <joe@gilith.com>
license
HOLLight
provenance
HOL Light theory extracted on 2011-02-19
show
Data.Bool
Files
Package tarball
bool-def-or-1.0.tgz
Theory file
bool-def-or.thy
(included in the package tarball)
Defined Constant
Data
Bool
∨
Theorem
⊦
(
∨
)
=
λ
p
q
.
∀
r
. (
p
⇒
r
)
⇒
(
q
⇒
r
)
⇒
r
Input Type Operators
→
bool
Input Constants
=
Data
Bool
∀
⇒