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