Old_HOL: Ord.thy@fd1be45b64bf (annotated)

145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	1	(* Title: HOL/Ord.thy
118 5b96b1252cdc HOL/Ord.thy,.ML: files now have header comments lcp parents: 0 diff changeset	2	ID: $Id$
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
118 5b96b1252cdc HOL/Ord.thy,.ML: files now have header comments lcp parents: 0 diff changeset	4	Copyright 1993 University of Cambridge
5b96b1252cdc HOL/Ord.thy,.ML: files now have header comments lcp parents: 0 diff changeset	5
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	6	The type class for ordered types (* FIXME improve comment *)
118 5b96b1252cdc HOL/Ord.thy,.ML: files now have header comments lcp parents: 0 diff changeset	7	*)
5b96b1252cdc HOL/Ord.thy,.ML: files now have header comments lcp parents: 0 diff changeset	8
0 7949f97df77a Initial revision clasohm parents: diff changeset	9	Ord = HOL +
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	10
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	11	axclass
0 7949f97df77a Initial revision clasohm parents: diff changeset	12	ord < term
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	13
0 7949f97df77a Initial revision clasohm parents: diff changeset	14	consts
7949f97df77a Initial revision clasohm parents: diff changeset	15	"<", "<=" :: "['a::ord, 'a] => bool" (infixl 50)
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	16	mono :: "['a::ord => 'b::ord] => bool" (monotonicity)
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	17	min, max :: "['a::ord, 'a] => 'a"
0 7949f97df77a Initial revision clasohm parents: diff changeset	18
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	19	defs
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	20	mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	21	min_def "min(a, b) == if(a <= b, a, b)"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	22	max_def "max(a, b) == if(a <= b, b, a)"
0 7949f97df77a Initial revision clasohm parents: diff changeset	23
7949f97df77a Initial revision clasohm parents: diff changeset	24	end
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 118 diff changeset	25

author	clasohm
	Wed, 02 Nov 1994 11:50:09 +0100
changeset 156	fd1be45b64bf
parent 145	a9f7ff3a464c
permissions	-rw-r--r--