Parents |
basic_hol |
Children |
hol |
Constants |
IsOneRep
|
BOOL → BOOL |
One
|
ONE |
Types |
ONE
|
Definitions |
IsOneRep
is_one_rep_def
|
⊢ ∃ one• ∀ x• IsOneRep x ⇔ x ⇔ one |
ONE
one_def1
|
⊢ ∃ f• TypeDefn IsOneRep f |
One
one_def
|
⊢ ∀ x• x = One |
Theorems |
one_fns_thm
|
⊢ ∀ f• f = (λ x• One) |