1open HolKernel Parse boolLib
2
3open SGAUnicodeMergeA1Theory SGAUnicodeMergeA2Theory
4
5val _ = new_theory "SGAUnicodeMergeB";
6val _ = set_grammar_ancestry ["SGAUnicodeMergeA1", "SGAUnicodeMergeA2"]
7
8
9val numfails = ref 0
10
11val thm1 = store_thm(
12  "thm1",
13  ``INTER A1 A2 = ��� A1 A2``, (* UOK *)
14  REWRITE_TAC[]) handle HOL_ERR _ => (numfails := 1; TRUTH)
15
16val thm2 = store_thm(
17  "thm2",
18  ``FUNION f1 f2 = f1 ��� f2``,  (* UOK *)
19  REWRITE_TAC[]) handle HOL_ERR _ => (numfails := !numfails + 1; TRUTH)
20
21val _ = if !numfails > 0 then
22          raise mk_HOL_ERR "SGA Unicode Test" ""
23                (Int.toString (!numfails) ^ " failures")
24        else ()
25
26val _ = export_theory();
27