src/HOL/UNITY/LessThan.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5232 e5a7cdd07ea5
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/LessThan
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 lessThan, greaterThan, atLeast, atMost
     7 *)
     8 
     9 LessThan = List +
    10 
    11 constdefs
    12 
    13   lessThan   :: "nat => nat set"
    14      "lessThan n == {i. i<n}"
    15 
    16   atMost   :: "nat => nat set"
    17      "atMost n == {i. i<=n}"
    18  
    19   greaterThan   :: "nat => nat set"
    20      "greaterThan n == {i. n<i}"
    21 
    22   atLeast   :: "nat => nat set"
    23      "atLeast n == {i. n<=i}"
    24 
    25 end