Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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 = 5489: int

See also

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