DB.thy

STRUCTURE

SYNOPSIS

Return the contents of a theory.

DESCRIPTION

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

class, data, listDB, theorems, match, new_theory