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