1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "C";
4open multiLib BTheory
5
6val _ = List.tabulate(10, genthms 500)
7
8
9
10val _ = export_theory();
11