(* :mode=isabelle-options: *) section "HOL-SPARK" option spark_prv : bool = true -- "produce proof review file after 'spark_end'"