author | paulson |
Mon, 25 Jun 2001 15:36:55 +0200 | |
changeset 11378 | 5c84a5ca3a21 |
parent 10214 | 77349ed89f45 |
child 11609 | 3f3d1add4d94 |
permissions | -rw-r--r-- |
(* Title: HOL/SetInterval.thy ID: $Id$ Author: Tobias Nipkow Copyright 2000 TU Muenchen lessThan, greaterThan, atLeast, atMost *) SetInterval = equalities + 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