# HG changeset patch
# User krauss
# Date 1162889983 -3600
# Node ID 803bc7672d17aa93c1766f8e7374254f7a844f55
# Parent  2f6e276bfb930d4aa12febcb9b09f8ec4a21288c
method exported

diff -r 2f6e276bfb93 -r 803bc7672d17 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 09:41:14 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Nov 07 09:59:43 2006 +0100
@@ -1,5 +1,5 @@
 (*  Title:       HOL/Tools/function_package/lexicographic_order.ML
-    ID:
+    ID:          $Id$
     Author:      Lukas Bulwahn, TU Muenchen
 
 Method for termination proofs with lexicographic orderings.
@@ -7,6 +7,7 @@
 
 signature LEXICOGRAPHIC_ORDER =
 sig
+    val lexicographic_order : Method.method
     val setup: theory -> theory
 end
 
@@ -238,6 +239,8 @@
             end
     end
 
-val setup = Method.add_methods [("lexicographic_order", Method.no_args (Method.SIMPLE_METHOD lexicographic_order_tac), "termination prover for lexicographic orderings")]
+val lexicographic_order = Method.SIMPLE_METHOD lexicographic_order_tac
+
+val setup = Method.add_methods [("lexicographic_order", Method.no_args lexicographic_order, "termination prover for lexicographic orderings")]
 
 end
\ No newline at end of file