Ancestors of theory Term

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 

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