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