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