xref: /seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/poly/holfoot-full.ML

use "corecl.ML";

fun main () = holfoot_run (true, use);