data
DB.type data
Type abbreviation used in DB structure.
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,
Located
{exact = true, linenum = 228, scriptpath =
"$(HOLDIR)/src/bool/boolScript.sml"}))]: public_data list