# HG changeset patch # User wenzelm # Date 1470500099 -7200 # Node ID 994d1a1105ef1679d6352c2a52d17511ee00d81e # Parent 1a38142e11727382250d5842b95bd955a8b4bec2 more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy; diff -r 1a38142e1172 -r 994d1a1105ef NEWS --- a/NEWS Sat Aug 06 17:39:21 2016 +0200 +++ b/NEWS Sat Aug 06 18:14:59 2016 +0200 @@ -57,6 +57,9 @@ theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order is relevant to avoid confusion of Pure.simp vs. HOL.simp. +* Commands 'prf' and 'full_prf' are somewhat more informative (again): +proof terms are reconstructed and cleaned from administrative thm nodes. + *** Prover IDE -- Isabelle/Scala/jEdit *** diff -r 1a38142e1172 -r 994d1a1105ef src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Aug 06 17:39:21 2016 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Aug 06 18:14:59 2016 +0200 @@ -84,10 +84,8 @@ \a\<^sub>1, \, a\<^sub>n\ do not have any permanent effect. \<^descr> @{command "prf"} displays the (compact) proof term of the current proof - state (if present), or of the given theorems. Note that this requires - proof terms to be switched on for the current object logic (see the - ``Proof terms'' section of the Isabelle reference manual for information - on how to do this). + state (if present), or of the given theorems. Note that this requires an + underlying logic image with proof terms enabled, e.g. \HOL-Proofs\. \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full proof term, i.e.\ also displays information omitted in the compact proof diff -r 1a38142e1172 -r 994d1a1105ef src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Aug 06 17:39:21 2016 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Aug 06 18:14:59 2016 +0200 @@ -258,9 +258,24 @@ (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf') end | SOME srcs => - let val ctxt = Toplevel.context_of state - in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end - |> Pretty.chunks); + let + val ctxt = Toplevel.context_of state; + val thy = Proof_Context.theory_of ctxt; + fun pretty_proof thm = + let + val (_, prop) = + Logic.unconstrainT (Thm.shyps_of thm) + (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); + in + Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) + |> Reconstruct.reconstruct_proof ctxt prop + |> Reconstruct.expand_proof ctxt [("", NONE)] + |> Proofterm.rew_proof thy + |> Proofterm.no_thm_proofs + |> not full ? Proofterm.shrink_proof + |> Proof_Syntax.pretty_proof ctxt + end; + in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end); fun string_of_prop ctxt s = let