listDB

DB.listDB : unit -> data list

All theorems, axioms, and definitions in the currently loaded theory segments.

An invocation listDB() returns everything that has been stored in all theory segments currently loaded.

Example

- length (listDB());
> val it = 736 : int

See also

DB.thy, DB.theorems, DB.definitions, DB.axioms, DB.find, DB.match