| changeset 0 | 7949f97df77a |
| child 118 | 5b96b1252cdc |
| -1:000000000000 | 0:7949f97df77a |
|---|---|
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 |