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
     1 (*  Title:      HOL/SetInterval.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000  TU Muenchen
     5 
     6 lessThan, greaterThan, atLeast, atMost
     7 *)
     8 
     9 SetInterval = equalities + Arith + 
    10 
    11 constdefs
    12  lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
    13 "{..u(} == {x. x<u}"
    14 
    15  atMost      :: "('a::ord) => 'a set"	("(1{.._})")
    16 "{..u} == {x. x<=u}"
    17 
    18  greaterThan :: "('a::ord) => 'a set"	("(1{')_..})")
    19 "{)l..} == {x. l<x}"
    20 
    21  atLeast     :: "('a::ord) => 'a set"	("(1{_..})")
    22 "{l..} == {x. l<=x}"
    23 
    24 end