author | clasohm |
Tue, 30 Jan 1996 15:24:36 +0100 | |
changeset 1465 | 5d7a7e439cec |
parent 1440 | de6f18da81bb |
child 1572 | dbecd983863f |
permissions | -rw-r--r-- |
(* Title: HOL/AxClasses/Lattice/ROOT.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders via axiomatic type classes. *) open AxClass; reset HOL_quantifiers; reset eta_contract; set show_types; set show_sorts; use "tools.ML"; use_thy "Order"; use_thy "OrdDefs"; use_thy "OrdInsts"; use_thy "Lattice"; use_thy "CLattice"; use_thy "LatPreInsts"; use_thy "LatInsts"; use_thy "LatMorph"; make_chart (); (*make HTML chart*)