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