author | berghofe |
Fri, 02 Aug 1996 12:25:26 +0200 | |
changeset 1899 | 0075a8d26a80 |
parent 1440 | de6f18da81bb |
child 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 < 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