author | lcp |
Thu, 06 Apr 1995 11:49:42 +0200 | |
changeset 246 | 0f9230a24164 |
parent 0 | 7949f97df77a |
permissions | -rw-r--r-- |
0 | 1 |
Ord = HOL + |
2 |
classes |
|
3 |
ord < term |
|
4 |
consts |
|
5 |
"<", "<=" :: "['a::ord, 'a] => bool" (infixl 50) |
|
6 |
mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) |
|
7 |
min,max :: "['a::ord,'a] => 'a" |
|
8 |
||
9 |
rules |
|
10 |
||
11 |
mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
12 |
min_def "min(a,b) == if(a <= b, a, b)" |
|
13 |
max_def "max(a,b) == if(a <= b, b, a)" |
|
14 |
||
15 |
end |