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

use "corecl.ML";

fun main () = holfoot_run (false, fn x => Parse.print_with_style [PPBackEnd.FG PPBackEnd.OrangeRed] "File mode not supported in compressed version!\n");