--- a/src/Pure/more_thm.ML Sat Nov 02 20:52:24 2019 +0000
+++ b/src/Pure/more_thm.ML Sat Nov 02 23:13:15 2019 +0100
@@ -113,6 +113,7 @@
val tag: string * string -> attribute
val untag: string -> attribute
val kind: string -> attribute
+ val expose_proofs: theory -> thm list -> unit
val reconstruct_proof_of: thm -> Proofterm.proof
val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
thm -> Proofterm.proof
@@ -654,6 +655,11 @@
(** proof terms **)
+fun expose_proofs thy thms =
+ if Proofterm.export_proof_boxes_required thy then
+ Proofterm.export_proof_boxes (map Thm.proof_of thms)
+ else ();
+
fun reconstruct_proof_of thm =
Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);