DB.data

STRUCTURE

SYNOPSIS

Type abbreviation used in DB structure.

DESCRIPTION

When functions from the DB structure are used to query the current theory, answer are often phrased in terms of the data type, which is a type abbreviation declared as

   type data = (string * string) * (thm * class)

An element ((thy,name), (th,cl)) means that th is a theorem with classification class, stored in theory segment thy under name.

EXAMPLE

- DB.find "BOOL_CASES_AX";
> val it = [(("bool", "BOOL_CASES_AX"),
            (|- !t. (t = T) \/ (t = F), Axm))]
   : ((string * string) * (thm * class)) list

SEEALSO

class, thy, find, match, apropos, listDB