1.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Sun May 29 19:05:14 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Tue May 31 09:16:12 2022 +0200
1.3 @@ -1,8 +1,6 @@
1.4 (* Title: BaseDefinitions/rewrite-order.sml
1.5 Author: Walther Neuper
1.6 (c) due to copyright terms
1.7 -
1.8 -TODO: use "Rewrite_Ord" for renaming identifiers.
1.9 *)
1.10 signature REWRITE_ORDER =
1.11 sig
1.12 @@ -13,6 +11,7 @@
1.13
1.14 type rew_ord = Rule_Def.rew_ord
1.15 val e_rew_ordX: rew_ord
1.16 + val to_string: rew_ord -> string
1.17
1.18 type rew_ord' = Rule_Def.rew_ord'
1.19 val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
1.20 @@ -33,6 +32,7 @@
1.21 type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
1.22 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
1.23 val e_rew_ordX = (e_rew_ord', e_rew_ord_)
1.24 +fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
1.25
1.26 type rew_ord' = Rule_Def.rew_ord'
1.27 (* rewrite orders, also stored in 'type met' and type 'and rls'