1open HolKernel Parse boolLib testutils
2
3val _ = new_theory "nullary_tgt";
4
5val _ = let
6  val _ = tprint "Testing creation of output file via Holmake"
7  val op++ = OS.Path.concat
8  val _ = OS.FileSys.chDir "test"
9  val _ = OS.FileSys.remove "output" handle _ => ()
10  val _ = Systeml.systeml [Systeml.HOLDIR ++ "bin" ++ "Holmake"]
11in
12  if OS.FileSys.access("output", []) then OK()
13  else die "FAILED!"
14end
15
16val _ = OS.FileSys.chDir OS.Path.parentArc
17
18val th = save_thm("th", TRUTH);
19
20
21val _ = export_theory();
22