1structure multiLib = 2struct 3 4open HolKernel boolLib 5fun genthms delay n = 6 let 7 val v = mk_var("v" ^ Int.toString n, bool) 8 val g = mk_imp(v,v) 9 in 10 store_thm(current_theory() ^ Int.toString n, g, 11 REWRITE_TAC[]) before 12 ignore (Posix.Process.sleep (Time.fromMilliseconds delay)) 13 end 14 15end 16