1structure updateSyntax :> updateSyntax =
2struct
3
4open Abbrev HolKernel updateTheory
5
6val monop = HolKernel.syntax_fns1 "update"
7val binop = HolKernel.syntax_fns2 "update"
8
9val monop3 =
10   HolKernel.syntax_fns {n = 3, dest = HolKernel.dest_monop,
11      make = Lib.curry boolSyntax.mk_icomb} "update"
12
13val (find_tm, mk_find, dest_find, is_find) = binop "FIND"
14
15val (override_tm, mk_override, dest_override, is_override) = monop "OVERRIDE"
16
17val (list_update_tm, mk_list_update, dest_list_update, is_list_update) =
18   monop3 "LIST_UPDATE"
19
20val strip_list_update =
21   List.map pairSyntax.dest_pair o fst o listSyntax.dest_list o dest_list_update
22
23end
24