src/HOL/SetInterval.thy
author paulson
Wed May 24 18:46:06 2000 +0200 (2000-05-24)
changeset 8957 26b6e8f43305
parent 8924 c434283b4cfa
child 10212 33fe2d701ddd
permissions -rw-r--r--
added parent
nipkow@8924
     1
(*  Title:      HOL/SetInterval.thy
nipkow@8924
     2
    ID:         $Id$
nipkow@8924
     3
    Author:     Tobias Nipkow
paulson@8957
     4
    Copyright   2000  TU Muenchen
nipkow@8924
     5
nipkow@8924
     6
lessThan, greaterThan, atLeast, atMost
nipkow@8924
     7
*)
nipkow@8924
     8
paulson@8957
     9
SetInterval = equalities + Arith + 
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