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