# HG changeset patch
# User nipkow
# Date 959059944 -7200
# Node ID c434283b4cfa71339d5b9001cdd1d6272175011d
# Parent  42fd7abde9aa3b4630e5a1bd6197cfa0899c7e76
Added SetInterval

diff -r 42fd7abde9aa -r c434283b4cfa src/HOL/Fun.thy
--- 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)
diff -r 42fd7abde9aa -r c434283b4cfa src/HOL/SetInterval.thy
--- /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