| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15178 | 5f621aa35c25 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Ordered Groups *} |
6 header {* Ordered Groups *} |
7 |
7 |
8 theory OrderedGroup |
8 theory OrderedGroup |
9 import Inductive LOrder |
9 imports Inductive LOrder |
10 files "../Provers/Arith/abel_cancel.ML" |
10 files "../Provers/Arith/abel_cancel.ML" |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 The theory of partially ordered groups is taken from the books: |
14 The theory of partially ordered groups is taken from the books: |