| changeset 8229 | 38f453607c61 |
| parent 7657 | dbbf7721126e |
| child 8301 | d9345bad5e5c |
| 8228:8283e416b680 | 8229:38f453607c61 |
|---|---|
50 theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
50 theorem [trans]: "[| x = y; y < z |] ==> x < z"; (* = < < *) |
51 by (rule ssubst); |
51 by (rule ssubst); |
52 |
52 |
53 theorems [trans] = trans (* = = = *) |
53 theorems [trans] = trans (* = = = *) |
54 |
54 |
55 theorems [elim??] = sym |
|
56 |
|
55 |
57 |
56 end; |
58 end; |