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