src/HOL/SetInterval.thy
author nipkow
Tue May 23 07:32:24 2000 +0200 (2000-05-23)
changeset 8924 c434283b4cfa
child 8957 26b6e8f43305
permissions -rw-r--r--
Added SetInterval
nipkow@8924
     1
(*  Title:      HOL/SetInterval.thy
nipkow@8924
     2
    ID:         $Id$
nipkow@8924
     3
    Author:     Tobias Nipkow
nipkow@8924
     4
    Copyright   1998  TU Muenchen
nipkow@8924
     5
nipkow@8924
     6
lessThan, greaterThan, atLeast, atMost
nipkow@8924
     7
*)
nipkow@8924
     8
nipkow@8924
     9
SetInterval = equalities +
nipkow@8924
    10
nipkow@8924
    11
constdefs
nipkow@8924
    12
 lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
nipkow@8924
    13
"{..u(} == {x. x<u}"
nipkow@8924
    14
nipkow@8924
    15
 atMost      :: "('a::ord) => 'a set"	("(1{.._})")
nipkow@8924
    16
"{..u} == {x. x<=u}"
nipkow@8924
    17
nipkow@8924
    18
 greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
nipkow@8924
    19
"{)l..} == {x. l<x}"
nipkow@8924
    20
nipkow@8924
    21
 atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
nipkow@8924
    22
"{l..} == {x. l<=x}"
nipkow@8924
    23
nipkow@8924
    24
end