(* side-entry for HOL-Main *) use_thys ["Main"];