exported mk_base_funs for use by size-change tools
authorkrauss
Fri, 24 Nov 2006 13:39:22 +0100
changeset 21510 7e72185e4b24
parent 21509 6c5755ad9cae
child 21511 16c62deb1adf
exported mk_base_funs for use by size-change tools
src/HOL/Tools/function_package/lexicographic_order.ML
--- 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