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", "RealFieldContext",
"sorting", "numeral_bit", "iterate", "fcp", "sum_num", "logroot", "bit",
"numposrep", "ternaryComparisons", "string", "ASCIInumbers", "words",
"bitstring", "ConseqConv", "quantHeuristics", "patternMatches",
"EnumTypeContext", "ordinalBasic", "bnfInitial", "permutes",
"hurdUtilsContext", "divides", "pred_set", "set_relation", "wellorder",
"cardinalityCore", "bnfPrelims", "bnfFixBNF", "bnfMutual", "While",
"NumConvContext", "cv", "BoolconvContext", "reduce", "SubAndCondContext",
"one", "sum", "option", "pairToolsContext", "numeral", "basicSize",
"numpair", "ind_type", "list", "rich_list", "indexedLists", "hol",
"quotient", "pair", "InductiveDefinitionContext", "Canon_Port_Context",
"mesonLibContext", "folMappingContext", "folToolsContext", "sat",
"canonContext", "combin", "boolSimpsContext", "normalForms",
"normalFormsContext", "relation", "min", "bool", "marker", "num",
"prim_rec", "arithmetic", "normalizer", "integer"]: string list