src/Pure/proof_general.ML
changeset 15238 cb559bd0b03c
parent 15225 68ab0f4eb457
child 15253 6e20cc79bde6
equal deleted inserted replaced
15237:250e9be7a09d 15238:cb559bd0b03c
   598      ("full-proofs", 
   598      ("full-proofs", 
   599       ("Record full proof objects internally",
   599       ("Record full proof objects internally",
   600        proof_option)),
   600        proof_option)),
   601      ("theorem-dependencies", 
   601      ("theorem-dependencies", 
   602        ("Track theorem dependencies within Proof General",
   602        ("Track theorem dependencies within Proof General",
   603 	thm_deps_option))])
   603 	thm_deps_option)),
       
   604      ("skip-proofs", 
       
   605       ("Skip all proof scripts (interactive-only)",
       
   606        bool_option Toplevel.skip_proofs))])
   604    ];
   607    ];
   605 end
   608 end
   606 
   609 
   607 (* Configuration: GUI config, proverinfo messages *)
   610 (* Configuration: GUI config, proverinfo messages *)
   608 
   611