src/HOL/SetInterval.thy

new definitions of fun_apply and M_is_recfun

(*  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