theorems

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

All the theorems stored in the named theory.

An invocation theorems thy, where thy is the name of a currently loaded theory segment, will return a list of the theorems stored in that theory. Axioms and definitions are excluded. 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

> theorems "combin";
val it =
   [("W_THM", ⊢ ∀f x. W f x = f x x),
    ("UPDATE_EQ", ⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ 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.
         f1⦇a ↦ b⦈ = f2⦇a ↦ c⦈ ⇒ b = c ∧ ∀v. f1⦇a ↦ v⦈ = f2⦇a ↦ v⦈),
[...Output elided...]

See also

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