1open HolKernel Parse boolLib
2
3val _ = new_theory "SGAUnicodeMergeA1";
4
5val UNION_def = new_definition(
6  "UNION_def",
7  ``UNION P Q x <=> P x \/ Q x``);
8
9val _ = export_theory();
10