Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/AxClasses/Lattice/LatInsts.thy
author berghofe
Fri, 02 Aug 1996 12:25:26 +0200
changeset 1899 0075a8d26a80
parent 1440 de6f18da81bb
child 2606 27cdd600a3b1
permissions -rw-r--r--
Classical tactics now use default claset.

(*  Title:      LatInsts.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Some lattice instantiations.
*)

LatInsts = LatPreInsts +


(* linear orders are lattices *)

instance
  lin_order < lattice                   (allI, exI, min_is_inf, max_is_sup)


(* complete lattices are lattices *)

instance
  clattice < lattice                    (allI, exI, Inf_is_inf, Sup_is_sup)


(* products of lattices are lattices *)

instance
  "*" :: (lattice, lattice) lattice     (allI, exI, prod_is_inf, prod_is_sup)

instance
  fun :: (term, lattice) lattice        (allI, exI, fun_is_inf, fun_is_sup)


(* duals of lattices are lattices *)

instance
  dual :: (lattice) lattice             (allI, exI, dual_is_inf, dual_is_sup)

(*FIXME bug workaround (see also OrdInsts.thy)*)
instance
  dual :: (lin_order) lin_order         (le_dual_lin)

end
isabelle