author | wenzelm |
Mon, 08 May 2000 20:59:30 +0200 | |
changeset 8840 | 18b76c137c41 |
parent 7626 | 5997f35954d7 |
permissions | -rw-r--r-- |
(* Title: HOL/BCV/SemiLattice.thy ID: $Id$ Author: Tobias Nipkow Copyright 1999 TUM Semilattices *) SemiLattice = Plus + constdefs semilat :: "('a::{order,plus} set) => bool" "semilat A == (!x:A. !y:A. x <= x+y) & (!x:A. !y:A. y <= x+y) & (!x:A. !y:A. !z:A. x <= z & y <= z --> x+y <= z) & (!x:A. !y:A. x+y : A)" end