author | wenzelm |
Wed, 12 Feb 1997 15:42:31 +0100 | |
changeset 2606 | 27cdd600a3b1 |
parent 1573 | 6d66b59f94a9 |
permissions | -rw-r--r-- |
(* Title: CLattice.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen Complete lattices are orders with infima and suprema of arbitrary subsets. TODO: derive some more well-known theorems (e.g. ex_Inf == ex_Sup) *) CLattice = Order + axclass clattice < partial_order ex_Inf "ALL A. EX inf. is_Inf A inf" ex_Sup "ALL A. EX sup. is_Sup A sup" constdefs Inf :: "'a::clattice set => 'a" "Inf A == @inf. is_Inf A inf" Sup :: "'a::clattice set => 'a" "Sup A == @sup. is_Sup A sup" end