1open HolKernel Parse boolLib Datatype
2
3val _ = new_theory "monofldA";
4
5val _ = Datatype`rcd = <| myset : 'a -> bool ; sz : num |>`;
6
7val _ = gen_remove_ovl_mapping
8          (GrammarSpecials.recfupd_special ^ "myset")
9          ``\f x. rcd_myset_fupd f x``
10
11val _ = Parse.add_record_fupdate(
12      "myset", Term.inst[beta |-> alpha] ``rcd_myset_fupd``);
13
14val _ = export_theory();
15