Ancestors of theory Example

The name of every theory is linked to its theory file
\/ stands for subtheories (child theories)
/\ stands for supertheories (parent theories)
... stands for repeated subtrees

Back to the index of Bali_ASCII2 

Example \/
 \__Eval \//\
     \__State \//\
     |   \__WellForm \//\
     |       \__WellType \//\
     |           \__TypeRel \//\
     |               \__Decl \//\
     |                   \__Term \//\
     |                       \__Type \//\
     |                           \__Table \//\
     |                               \__Basis \//\
     |                                   \__Sum \//\
     |                                   |   \__mono \//\
     |                                   |   |   \__equalities \//\
     |                                   |   |       \__subset \//\
     |                                   |   |           \__Fun \//\
     |                                   |   |               \__Vimage \//\
     |                                   |   |                   \__Set \//\
     |                                   |   |                       \__Ord \//\
     |                                   |   |                           \__HOL \//\
     |                                   |   |                               \__CPure \/
     |                                   |   \__Prod \//\
     |                                   |       \__Fun...\//\
     |                                   \__WF_Rel \//\
     |                                   |   \__Finite \//\
     |                                   |       \__Divides \//\
     |                                   |       |   \__Arith \//\
     |                                   |       |       \__Nat \//\
     |                                   |       |           \__NatDef \//\
     |                                   |       |               \__WF \//\
     |                                   |       |                   \__Trancl \//\
     |                                   |       |                       \__Lfp \//\
     |                                   |       |                       |   \__mono...\//\
     |                                   |       |                       \__Relation \//\
     |                                   |       |                           \__Prod...\//\
     |                                   |       \__Power \//\
     |                                   |           \__Divides...\//\
     |                                   \__Map \//\
     |                                   |   \__List \//\
     |                                   |   |   \__WF_Rel...\//\
     |                                   |   \__Option \//\
     |                                   |       \__Arith...\//\
     |                                   \__IntDef \//\
     |                                   |   \__Equiv \//\
     |                                   |   |   \__Relation...\//\
     |                                   |   \__Arith...\//\
     |                                   \__Inductive \//\
     |                                       \__Gfp \//\
     |                                       |   \__Lfp...\//\
     |                                       \__Prod...\//\
     \__inductive2 \//\
         \__Gfp...\//\