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