(* Title:  BaseDefinitions/rewrite-order.sml

    Author: Walther Neuper

    (c) due to copyright terms

 *)

 signature REWRITE_ORDER =

 sig

   type id = Rule_Def.rew_ord_id

   val id_empty: id

   type function = Rule_Def.rew_ord_function

   val function_empty: function

   type T = Rule_Def.rew_ord_T

   val empty: T

   val to_string: T -> string

   val equal: T * T -> bool

 end

 (**)

 structure Rewrite_Ord(**): REWRITE_ORDER(**) =

 struct

 (**)

 type id = Rule_Def.rew_ord_id

 val id_empty = "Rewrite_Ord.id_empty";

 type function = Rule_Def.rew_ord_function;

 fun function_empty (_: Proof.context) (_: LibraryC.subst) (_: term, _: term) = true;

 type T = Rule_Def.rew_ord_T

 val empty = (id_empty, function_empty)

 fun to_string (rew_ord, _) = "(" ^ rew_ord ^ ", _: fn)"

 fun equal ((id1, _), (id2, _)) = id1 = id2

 end