1signature updateLib =
2sig
3    include Abbrev
4
5    val strip_list_update        : term -> (term * term) list
6
7    val UPDATE_APPLY_CONV       : conv -> conv
8
9    val LIST_UPDATE_INTRO_CONV  : conv
10    val LIST_UPDATE_ELIM_CONV   : conv
11
12    val OVERRIDE_UPDATES_CONV   : hol_type -> conv -> conv
13    val SORT_UPDATES_CONV       : term -> computeLib.compset -> conv -> conv
14    val SORT_UPDATES_MAPTO_CONV : term -> term -> computeLib.compset -> conv ->
15                                  conv
16
17    val SORT_NUM_UPDATES_CONV   : conv
18    val SORT_WORD_UPDATES_CONV  : hol_type -> conv
19    val SORT_ENUM_UPDATES_CONV  : hol_type -> conv
20end
21