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