src/HOL/UNITY/LessThan.thy
changeset 4776 1f9362e769c1
child 5232 e5a7cdd07ea5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/LessThan.thy	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(*  Title:      HOL/UNITY/LessThan
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +lessThan, greaterThan, atLeast, atMost
    1.10 +*)
    1.11 +
    1.12 +LessThan = List +
    1.13 +
    1.14 +constdefs
    1.15 +
    1.16 +  lessThan   :: "nat => nat set"
    1.17 +     "lessThan n == {i. i<n}"
    1.18 +
    1.19 +  atMost   :: "nat => nat set"
    1.20 +     "atMost n == {i. i<=n}"
    1.21 + 
    1.22 +  greaterThan   :: "nat => nat set"
    1.23 +     "greaterThan n == {i. n<i}"
    1.24 +
    1.25 +  atLeast   :: "nat => nat set"
    1.26 +     "atLeast n == {i. n<=i}"
    1.27 +
    1.28 +end