Package axiom-choice: axiom-choice
Information
name
axiom-choice
version
1.0
description
axiom-choice
author
Joe Hurd <joe@gilith.com>
license
HOLLight
provenance
HOL Light theory extracted on 2011-02-19
show
Data.Bool
Files
Package tarball
axiom-choice-1.0.tgz
Theory file
axiom-choice.thy
(included in the package tarball)
Theorem
⊦
∀
P
x
.
P
x
⇒
P
((
select
)
P
)
Input Type Operators
→
bool
Input Constants
Data
Bool
∀
⇒
select
Assumption
⊦
∀
P
x
.
P
x
⇒
P
((
select
)
P
)