equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature LEXICOGRAPHIC_ORDER = |
8 signature LEXICOGRAPHIC_ORDER = |
9 sig |
9 sig |
10 val lexicographic_order : Proof.context -> Method.method |
10 val lexicographic_order : Proof.context -> Method.method |
|
11 |
|
12 (* exported for use by size-change termination prototype. |
|
13 FIXME: provide a common interface later *) |
|
14 val mk_base_funs : typ -> term list |
|
15 |
11 val setup: theory -> theory |
16 val setup: theory -> theory |
12 end |
17 end |
13 |
18 |
14 structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
19 structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
15 struct |
20 struct |