author | wenzelm |
Tue, 17 Nov 1998 14:07:25 +0100 | |
changeset 5906 | 1f58694fc3e2 |
parent 5536 | 130f3d891fb2 |
child 7878 | 43b03d412b82 |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/LessThan ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge lessThan, greaterThan, atLeast, atMost Could generalize to any linear ordering? *) LessThan = Main + constdefs lessThan :: "nat => nat set" "lessThan n == {i. i<n}" atMost :: "nat => nat set" "atMost n == {i. i<=n}" greaterThan :: "nat => nat set" "greaterThan n == {i. n<i}" atLeast :: "nat => nat set" "atLeast n == {i. n<=i}" end