print_theory

Hol_pp.print_theory : string -> unit

Print a theory on the standard output.

An invocation print_theory s will display the contents of the theory segment s on the standard output. The string "-" may be used to denote the current theory segment.

Failure

If s is not the name of a loaded theory.

Example

> print_theory "combin";
Theory: combin

Parents:
    marker

Term constants:
    :>            :β -> (β -> α) -> α
    ASSOC         :(α -> α -> α) -> bool
    C             :(α -> β -> γ) -> β -> α -> γ
    COMM          :(α -> α -> β) -> bool
    EXTENSIONAL   :(α -> bool) -> (α -> β) -> bool
    FAIL          :α -> β -> α
    FCOMM         :(α -> β -> α) -> (γ -> α -> α) -> bool
    I             :α -> α
    K             :α -> β -> α
    LEFT_ID       :(α -> β -> β) -> α -> bool
    MONOID        :(α -> α -> α) -> α -> bool
    RESTRICTION   :(α -> bool) -> (α -> β) -> α -> β
    RIGHT_ID      :(α -> β -> α) -> β -> bool
    S             :(α -> β -> γ) -> (α -> β) -> α -> γ
    UPDATE        :α -> β -> (α -> β) -> α -> β
    W             :(α -> α -> β) -> α -> β
    o             :(γ -> β) -> (α -> γ) -> α -> β

Definitions:
    APP_DEF
      ⊢ ∀x f. (x :> f) = f x
    ASSOC_DEF
      ⊢ ∀f. ASSOC f ⇔ ∀x y z. f x (f y z) = f (f x y) z
    COMM_DEF
      ⊢ ∀f. COMM f ⇔ ∀x y. f x y = f y x
    C_DEF
      ⊢ flip = (λf x y. f y x)
    EXTENSIONAL_def
      ⊢ ∀s f. EXTENSIONAL s f ⇔ ∀x. x ∉ s ⇒ f x = ARB
    FAIL_DEF
      ⊢ FAIL = (λx y. x)
    FCOMM_DEF
      ⊢ ∀f g. FCOMM f g ⇔ ∀x y z. g x (f y z) = f (g x y) z
    I_DEF
      ⊢ I = S K K
    K_DEF
      ⊢ K = (λx y. x)
    LEFT_ID_DEF
      ⊢ ∀f e. LEFT_ID f e ⇔ ∀x. f e x = x
    MONOID_DEF
      ⊢ ∀f e. MONOID f e ⇔ ASSOC f ∧ RIGHT_ID f e ∧ LEFT_ID f e
    RESTRICTION
      ⊢ ∀s f x. RESTRICTION s f x = if x ∈ s then f x else ARB
    RIGHT_ID_DEF
[...Output elided...]

See also

DB.dest_theory, DB.thy