1open HolKernel Parse boolLib
2
3val _ = new_theory "mergeGrammarsA2";
4
5(* see comment at head of mergeGrammarsA1Script for description of what is
6   being tested
7*)
8
9val a_theorem = store_thm(
10  "a_theorem",
11  ``(x:bool = x) /\ (y = y)``,
12  REWRITE_TAC[]);
13
14
15val _ = export_theory();
16