Added SetInterval

--- a/src/HOL/Fun.thy	Mon May 22 16:05:22 2000 +0200
+++ b/src/HOL/Fun.thy	Tue May 23 07:32:24 2000 +0200
@@ -6,7 +6,7 @@
 Notions about functions.
 *)
 
-Fun = Vimage + equalities + 
+Fun = Vimage + SetInterval + 
 
 instance set :: (term) order
                        (subset_refl,subset_trans,subset_antisym,psubset_eq)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SetInterval.thy	Tue May 23 07:32:24 2000 +0200
@@ -0,0 +1,24 @@
+(*  Title:      HOL/SetInterval.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998  TU Muenchen
+
+lessThan, greaterThan, atLeast, atMost
+*)
+
+SetInterval = equalities +
+
+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