| changeset 5953 | d6017ce6b93e |
| parent 5889 | d3ecef6b5682 |
| child 6402 | 2b23e14dd386 |
| 5952:7d4ec8992b23 | 5953:d6017ce6b93e |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 Ord = HOL + |
9 Ord = HOL + |
10 |
10 |
11 (*FIXME move to HOL.thy*) |
11 (*FIXME move to HOL.thy*) |
12 setup attrib_setup |
|
12 setup Classical.setup |
13 setup Classical.setup |
13 setup attrib_setup |
14 setup Blast.setup |
15 setup Clasimp.setup |
|
16 |
|
14 |
17 |
15 axclass |
18 axclass |
16 ord < term |
19 ord < term |
17 |
20 |
18 global |
21 global |