1open HolKernel Parse BasicProvers simpLib Datatype 2 3val _ = new_theory "recordEnumSimpsB" 4 5local open recordEnumSimpsLib recordEnumSimpsATheory in end; 6 7val enum_lemma1 = Q.store_thm("enum_lemma1", 8 ���C2 <> C3���, 9 simp_tac (srw_ss()) []); 10 11val enum_lemma2 = Q.store_thm("enum_lemma2", 12 ���D10 <> D11���, 13 simp_tac (srw_ss()) []); 14 15val recd_lemma1 = Q.store_thm("recd_lemma1", 16 ���(r with fld1 := 3).fld1 = 3���, 17 simp_tac (srw_ss()) []); 18 19val recd_lemma2 = Q.store_thm("recd_lemma2", 20 ���(r with fld1 := 3).fld2 = r.fld2���, 21 simp_tac (srw_ss()) []); 22 23val normal_lemma = Q.store_thm("normal_lemma", 24 ���E1 n <> E3���, 25 computeLib.EVAL_TAC); 26 27val _ = export_theory(); 28