--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sig Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,22 @@
+(* ========================================================================= *)
+(* THE KNUTH-BENDIX TERM ORDERING *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature KnuthBendixOrder =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* The weight of all constants must be at least 1, and there must be at most *)
+(* one unary function with weight 0. *)
+(* ------------------------------------------------------------------------- *)
+
+type kbo =
+ {weight : Term.function -> int,
+ precedence : Term.function * Term.function -> order}
+
+val default : kbo
+
+val compare : kbo -> Term.term * Term.term -> order option
+
+end