HOL: Reference

thms

DB.thms : string -> (string * thm) list

All the theorems, definitions, and axioms stored in the named theory.

An invocation thms thy, where thy is the name of a currently loaded theory segment, will return a list of the theorems, definitions, and axioms stored in that theory. Each theorem is paired with its name in the result. The string "-" may be used to denote the current theory segment.

Failure

Never fails. If thy is not the name of a currently loaded theory segment, the empty list is returned.

Example

> thms "combin";
val it =
   [("W_THM", ⊢ ∀f x. W f x = f x x), ("W_DEF", ⊢ W = (λf x. f x x)),
    ("UPDATE_EQ", ⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ c⦈),
    ("UPDATE_def", ⊢ ∀a b. (a =+ b) = (λf c. if a = c then b else f c)),
    ("UPDATE_COMMUTES",
     ⊢ ∀f a b c d. a ≠ b ⇒ f⦇a ↦ c; b ↦ d⦈ = f⦇b ↦ d; a ↦ c⦈),
    ("UPDATE_APPLY_IMP_ID", ⊢ ∀f b a. f a = b ⇒ f⦇a ↦ b⦈ = f),
    ("UPDATE_APPLY_ID_RWT",
     ⊢ (∀f a b. f⦇a ↦ b⦈ = f ⇔ f a = b) ∧ ∀f a b. f = f⦇a ↦ b⦈ ⇔ f a = b),
    ("UPDATE_APPLY_ID", ⊢ ∀f a b. f a = b ⇔ f⦇a ↦ b⦈ = f),
    ("UPDATE_APPLY1", ⊢ ∀a x f. f⦇a ↦ x⦈ a = x),
    ("UPDATE_APPLY",
     ⊢ (∀a x f. f⦇a ↦ x⦈ a = x) ∧ ∀a b x f. a ≠ b ⇒ f⦇a ↦ x⦈ b = f b),
    ("UPD_SAME_KEY_UNWIND",
     ⊢ ∀f1 f2 a b c.
[...Output elided...]

See also

DB.thy, DB.theorems, DB.axioms, DB.definitions, DB.fetch, DB.listDB