| changeset 21382 | d71aed9286d3 |
| parent 21328 | 73bb86d0f483 |
| child 22390 | 378f34b1e380 |
| 21381:79e065f2be95 | 21382:d71aed9286d3 |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Ordered Groups *} |
7 header {* Ordered Groups *} |
8 |
8 |
9 theory OrderedGroup |
9 theory OrderedGroup |
10 imports Set LOrder |
10 imports LOrder |
11 uses "~~/src/Provers/Arith/abel_cancel.ML" |
11 uses "~~/src/Provers/Arith/abel_cancel.ML" |
12 begin |
12 begin |
13 |
13 |
14 text {* |
14 text {* |
15 The theory of partially ordered groups is taken from the books: |
15 The theory of partially ordered groups is taken from the books: |