| changeset 45778 | df6e210fb44c |
| parent 43269 | 3535f16d9714 |
| child 72004 | 913162a47d9f |
--- a/src/Tools/Metis/src/ElementSet.sml Wed Dec 07 15:10:29 2011 +0100 +++ b/src/Tools/Metis/src/ElementSet.sml Wed Dec 07 16:03:05 2011 +0100 @@ -16,6 +16,10 @@ type element = KM.key; +val compareElement = KM.compareKey; + +val equalElement = KM.equalKey; + (* ------------------------------------------------------------------------- *) (* A type of finite sets. *) (* ------------------------------------------------------------------------- *)