etc/options

 
 
 section "Theory Export"
 
 option export_document : bool = false
+  -- "export document sources to Isabelle/Scala"
 
 option export_theory : bool = false
+  -- "export theory content to Isabelle/Scala"
+
+option export_proofs : bool = false
+  -- "export proof terms to Isabelle/Scala"
+
+option prune_proofs : bool = false
+  -- "prune proof terms after export (do not store in Isabelle/ML)"
 
 
 section "Theory update"
 
 option update_inner_syntax_cartouches : bool = false