ancestry

Theory.ancestry : string -> string list

Returns the (proper) ancestry of a theory in a list.

A call to ancestry thy returns a list of all the proper ancestors (i.e. parents, parents of parents, etc.) of the theory thy. The shorthand "-" may be used to denote the name of the current theory segment.

Failure

Fails if thy is not an ancestor of the current theory.

Example

> load "bossLib";
val it = (): unit

> current_theory();
val it = "wombat": string

> ancestry "-";
val it =
   ["hrat", "hreal", "realax", "real_arith", "real", "sorting", "scratch",
    "numeral_bit", "permutes", "iterate", "fcp", "sum_num", "logroot", "bit",
    "numposrep", "ternaryComparisons", "string", "ASCIInumbers", "words",
    "bitstring", "ConseqConv", "quantHeuristics", "patternMatches",
    "ind_type", "divides", "While", "cv", "reduce", "one", "sum", "option",
    "numeral", "basicSize", "numpair", "pred_set", "list", "rich_list",
    "indexedLists", "hol", "quotient", "pair", "combin", "sat",
    "normalForms", "relation", "min", "bool", "marker", "num", "prim_rec",
    "arithmetic", "normalizer", "integer", "example"]: string list

See also

Theory.parents