src/HOL/AxClasses/Lattice/ROOT.ML
changeset 9000 c20d58286a51
parent 7240 a509730e424b
equal deleted inserted replaced
8999:ad8260dc6e4a 9000:c20d58286a51
     9 
     9 
    10 reset eta_contract;
    10 reset eta_contract;
    11 set show_types;
    11 set show_types;
    12 set show_sorts;
    12 set show_sorts;
    13 
    13 
    14 use_thy "Order";
    14 time_use_thy "Order";
    15 use_thy "OrdDefs";
    15 time_use_thy "OrdDefs";
    16 use_thy "OrdInsts";
    16 time_use_thy "OrdInsts";
    17 
    17 
    18 use_thy "Lattice";
    18 time_use_thy "Lattice";
    19 use_thy "CLattice";
    19 time_use_thy "CLattice";
    20 
    20 
    21 use_thy "LatPreInsts";
    21 time_use_thy "LatPreInsts";
    22 use_thy "LatInsts";
    22 time_use_thy "LatInsts";
    23 
    23 
    24 use_thy "LatMorph";
    24 time_use_thy "LatMorph";