1open HolKernel Parse boolLib bossLib; 2 3open simp_attr1Theory 4 5val _ = new_theory "simp_attr2"; 6 7val fact_SUC = store_thm( 8 "fact_SUC", 9 ``fact (SUC n) = SUC n * fact n``, 10 SRW_TAC [][]) 11 12val _ = export_theory(); 13