| author | lcp |
| Wed, 25 May 1994 12:43:50 +0200 | |
| changeset 76 | fb4fe9f8c3cd |
| parent 0 | 7949f97df77a |
| 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 |