author | wenzelm |
Wed, 03 Feb 1999 17:34:27 +0100 | |
changeset 6216 | 05d99c0bbfa0 |
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