equal
deleted
inserted
replaced
29 fun function_empty (_: LibraryC.subst) (_: term, _: term) = true; |
29 fun function_empty (_: LibraryC.subst) (_: term, _: term) = true; |
30 |
30 |
31 type T = Rule_Def.rew_ord_T |
31 type T = Rule_Def.rew_ord_T |
32 val empty = (id_empty, function_empty) |
32 val empty = (id_empty, function_empty) |
33 |
33 |
34 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)" |
34 fun to_string (rew_ord, _) = "(" ^ rew_ord ^ ", _: fn)" |
35 fun equal ((id1, _), (id2, _)) = id1 = id2 |
35 fun equal ((id1, _), (id2, _)) = id1 = id2 |
36 |
36 |
37 end |
37 end |