author | paulson |
Wed, 05 Nov 1997 13:23:46 +0100 | |
changeset 4153 | e534c4c32d54 |
parent 2606 | 27cdd600a3b1 |
permissions | -rw-r--r-- |
(* Title: Lattice.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen Lattices are orders with binary (finitary) infima and suprema. *) Lattice = Order + axclass lattice < partial_order ex_inf "ALL x y. EX inf. is_inf x y inf" ex_sup "ALL x y. EX sup. is_sup x y sup" consts "&&" :: "['a::lattice, 'a] => 'a" (infixl 70) "||" :: "['a::lattice, 'a] => 'a" (infixl 65) defs inf_def "x && y == @inf. is_inf x y inf" sup_def "x || y == @sup. is_sup x y sup" end