equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature LEXICOGRAPHIC_ORDER = |
8 signature LEXICOGRAPHIC_ORDER = |
9 sig |
9 sig |
10 val lexicographic_order : thm list -> Proof.context -> Method.method |
10 val lexicographic_order : thm list -> Proof.context -> Method.method |
11 |
11 val lexicographic_order_tac : Proof.context -> tactic -> tactic |
12 (* exported for debugging *) |
12 |
13 val setup: theory -> theory |
13 val setup: theory -> theory |
14 end |
14 end |
15 |
15 |
16 structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
16 structure LexicographicOrder : LEXICOGRAPHIC_ORDER = |
17 struct |
17 struct |