----------------------------------------------------------------------
thy                                                               (DB)
----------------------------------------------------------------------
thy : string -> data list

SYNOPSIS
Return the contents of a theory.

KEYWORDS
theory.

DESCRIBE
An invocation {DB.thy s} returns the contents of the specified theory segment
{s} in a list of {(thy,name),(thm,class)} tuples. In a tuple,
{(thy,name)} designate the theory and the name given to the object
in the theory. The {thm} element is the named object, and {class} its
classification (one of {Thm} (theorem), {Axm} (axiom), or {Def} (definition)).

Case distinctions are ignored when determining the segment. The current
segment may be specified, either by the distinguished literal {"-"},
or by the name given when creating the segment with {new_theory}.

FAILURE
Never fails, but will return an empty list when {s} does not designate
a currently loaded theory segment.

EXAMPLE

- DB.thy "pair";
> val it =
    [(("pair", "ABS_PAIR_THM"), (|- !x. ?q r. x = (q,r), Db.Thm)),
     (("pair", "ABS_REP_prod"),
      (|- (!a. ABS_prod (REP_prod a) = a) /\
          !r. IS_PAIR r = (REP_prod (ABS_prod r) = r), Db.Def)),
     (("pair", "CLOSED_PAIR_EQ"),
      (|- !x y a b. ((x,y) = (a,b)) = (x = a) /\ (y = b), Db.Thm)),
         .
         .
         .




SEEALSO
DB.class, DB.data, DB.listDB, DB.theorems, DB.match,
Theory.new_theory.

----------------------------------------------------------------------