src/HOL/AxClasses/Lattice/ROOT.ML
author wenzelm
Mon Jan 15 15:49:21 1996 +0100 (1996-01-15)
changeset 1440 de6f18da81bb
child 1572 dbecd983863f
permissions -rw-r--r--
added this stuff;
     1 (*  Title:      HOL/AxClasses/Lattice/ROOT.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Basic theory of lattices and orders via axiomatic type classes.
     6 *)
     7 
     8 open AxClass;
     9 
    10 reset HOL_quantifiers;
    11 reset eta_contract;
    12 set show_types;
    13 set show_sorts;
    14 
    15 use "tools.ML";
    16 
    17 use_thy "Order";
    18 use_thy "OrdDefs";
    19 use_thy "OrdInsts";
    20 
    21 use_thy "Lattice";
    22 use_thy "CLattice";
    23 
    24 use_thy "LatPreInsts";
    25 use_thy "LatInsts";
    26 
    27 use_thy "LatMorph";
    28 
    29 make_chart ();   (*make HTML chart*)