Ancestors of theory TypeRel

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 

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...\//\