Created:
V| 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) |