src/HOL/SetInterval.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8957 26b6e8f43305
child 10212 33fe2d701ddd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.

(*  Title:      HOL/SetInterval.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000  TU Muenchen

lessThan, greaterThan, atLeast, atMost
*)

SetInterval = equalities + Arith + 

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