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