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