author | paulson |
Thu, 17 Jan 2002 12:45:52 +0100 | |
changeset 12789 | 459b5de466b2 |
parent 11479 | 697dcaaf478f |
child 14046 | 6616e6c53d48 |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/UNITYMisc.thy ID: $Id$ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge Some miscellaneous and add-hoc set theory concepts. *) UNITYMisc = Main + constdefs less_than :: i=>i "less_than(A) == measure(A, %x. x)" lessThan :: [i, i] => i "lessThan(u,A) == {x:A. x<u}" greaterThan :: [i,i]=> i "greaterThan(u,A) == {x:A. u<x}" (* Identity relation over a domain A *) Identity :: i=>i "Identity(A) == {p:A*A. EX x. p=<x,x>}" end