eliminated theories "equalities" and "mono" (made part of "Typedef",
which supercedes "subset");
(* Title: HOL/SetInterval.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 2000 TU Muenchen
lessThan, greaterThan, atLeast, atMost
*)
SetInterval = NatArith +
constdefs
lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")
"{..u(} == {x. x<u}"
atMost :: "('a::ord) => 'a set" ("(1{.._})")
"{..u} == {x. x<=u}"
greaterThan :: "('a::ord) => 'a set" ("(1{')_..})")
"{)l..} == {x. l<x}"
atLeast :: "('a::ord) => 'a set" ("(1{_..})")
"{l..} == {x. l<=x}"
end