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