author | krauss |
Fri, 24 Nov 2006 13:39:22 +0100 | |
changeset 21510 | 7e72185e4b24 |
parent 21509 | 6c5755ad9cae |
child 21511 | 16c62deb1adf |
src/HOL/Tools/function_package/lexicographic_order.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Fri Nov 24 13:24:30 2006 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Fri Nov 24 13:39:22 2006 +0100 @@ -8,6 +8,11 @@ signature LEXICOGRAPHIC_ORDER = sig val lexicographic_order : Proof.context -> Method.method + + (* exported for use by size-change termination prototype. + FIXME: provide a common interface later *) + val mk_base_funs : typ -> term list + val setup: theory -> theory end