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
paulson@4776
     1
(*  Title:      HOL/UNITY/LessThan
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
lessThan, greaterThan, atLeast, atMost
paulson@4776
     7
*)
paulson@4776
     8
paulson@4776
     9
LessThan = List +
paulson@4776
    10
paulson@4776
    11
constdefs
paulson@4776
    12
paulson@4776
    13
  lessThan   :: "nat => nat set"
paulson@4776
    14
     "lessThan n == {i. i<n}"
paulson@4776
    15
paulson@4776
    16
  atMost   :: "nat => nat set"
paulson@4776
    17
     "atMost n == {i. i<=n}"
paulson@4776
    18
 
paulson@4776
    19
  greaterThan   :: "nat => nat set"
paulson@4776
    20
     "greaterThan n == {i. n<i}"
paulson@4776
    21
paulson@4776
    22
  atLeast   :: "nat => nat set"
paulson@4776
    23
     "atLeast n == {i. n<=i}"
paulson@4776
    24
paulson@4776
    25
end