The Theory one
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)

up quick index

privacy policy

Created:

V