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