constants

Theory.constants : string -> term list

Returns a list of the constants defined in a named theory.

The call

   constants thy

where thy is an ancestor theory (the special string "-" means the current theory), returns a list of all the constants in that theory.

Failure

Fails if the named theory does not exist, or is not an ancestor of the current theory.

Example

> load "combinTheory";
val it = (): unit

> constants "combin";
val it =
   [“$o”, “W”, “UPDATE”, “S”, “RIGHT_ID”, “RESTRICTION”, “MONOID”, “LEFT_ID”,
    “K”, “I”, “FCOMM”, “FAIL”, “EXTENSIONAL”, “COMM”, “flip”, “ASSOC”, “$:>”]:
   term list

See also

Theory.types, Theory.current_axioms, Theory.current_definitions, Theory.current_theorems