| author | lcp |
| Thu, 21 Jul 1994 10:52:00 +0200 | |
| changeset 97 | 3f4976d8c97f |
| parent 0 | 7949f97df77a |
| child 118 | 5b96b1252cdc |
| permissions | -rw-r--r-- |
| 0 | 1 |
open Ord; |
2 |
||
3 |
val [prem] = goalw Ord.thy [mono_def] |
|
4 |
"[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
|
5 |
by (REPEAT (ares_tac [allI, impI, prem] 1)); |
|
6 |
val monoI = result(); |
|
7 |
||
8 |
val [major,minor] = goalw Ord.thy [mono_def] |
|
9 |
"[| mono(f); A <= B |] ==> f(A) <= f(B)"; |
|
10 |
by (rtac (major RS spec RS spec RS mp) 1); |
|
11 |
by (rtac minor 1); |
|
12 |
val monoD = result(); |
|
13 |