1open HolKernel Parse boolLib 2 3val _ = new_theory "SGAUnicodeMergeA2"; 4 5val INTER_def = new_definition( 6 "INTER_def", 7 ``INTER P Q x = P x /\ Q x``); 8 9val _ = Unicode.unicode_version { u = "���", tmnm = "INTER"}; (* UOK *) 10 11val FUNION_def = new_definition( 12 "FUNION_def", 13 ``FUNION f1 f2 x <=> f1 x \/ f2 x``); 14 15val funion_symbol = UTF8.chr 0x228C 16val _ = set_fixity funion_symbol (Infixl 500) 17val _ = overload_on (funion_symbol, ``FUNION``) 18 19val _ = export_theory(); 20