1local 2 open HolKernel boolLib bossLib; 3 val holfoot_base_dir = Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/"; 4 val use_polyml = (Systeml.ML_SYSNAME = "poly") andalso 5 (Lib.mem "holfoot.state" (Portable.listDir (holfoot_base_dir^"poly")) handle SysErr _ => false) 6 val mldir = if use_polyml then "poly" else "mosml"; 7 val usefile = concat [holfoot_base_dir, mldir, "/header.sml"]; 8in 9 val _ = use usefile; 10end; 11