listDB : unit -> data list
STRUCTURE
DB
SYNOPSIS
All theorems, axioms, and definitions in the currently loaded theory segments.
DESCRIPTION
An invocation
listDB()
returns everything that has been stored in all theory segments currently loaded.
EXAMPLE
- length (listDB()); > val it = 736 : int
SEEALSO
thy
,
theorems
,
definitions
,
axioms
,
find
,
match
HOL
Kananaskis-10