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