1187 @{index_ML_type proof_body} \\ |
1187 @{index_ML_type proof_body} \\ |
1188 @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\ |
1188 @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\ |
1189 @{index_ML Proofterm.reconstruct_proof: |
1189 @{index_ML Proofterm.reconstruct_proof: |
1190 "theory -> term -> proof -> proof"} \\ |
1190 "theory -> term -> proof -> proof"} \\ |
1191 @{index_ML Proofterm.expand_proof: "theory -> |
1191 @{index_ML Proofterm.expand_proof: "theory -> |
1192 (string * term option) list -> proof -> proof"} \\ |
1192 (Proofterm.thm_header -> string option) -> proof -> proof"} \\ |
1193 @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ |
1193 @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ |
1194 @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ |
1194 @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ |
1195 @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ |
1195 @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ |
1196 \end{mldecls} |
1196 \end{mldecls} |
1197 |
1197 |
1226 Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not |
1226 Reconstruction may fail if \<open>prf\<close> is not a proof of \<open>prop\<close>, or if it does not |
1227 contain sufficient information for reconstruction. Failure may only happen |
1227 contain sufficient information for reconstruction. Failure may only happen |
1228 for proofs that are constructed manually, but not for those produced |
1228 for proofs that are constructed manually, but not for those produced |
1229 automatically by the inference kernel. |
1229 automatically by the inference kernel. |
1230 |
1230 |
1231 \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>thy [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> expands and |
1231 \<^descr> \<^ML>\<open>Proofterm.expand_proof\<close>~\<open>thy expand prf\<close> reconstructs and expands |
1232 reconstructs the proofs of all specified theorems, with the given (full) |
1232 the proofs of nested theorems according to the given \<open>expand\<close> function: a |
1233 proof. Theorems that are not unique specified via their name may be |
1233 result of @{ML \<open>SOME ""\<close>} means full expansion, @{ML \<open>SOME\<close>}~\<open>name\<close> means to |
1234 disambiguated by giving their proposition. |
1234 keep the theorem node but replace its internal name, @{ML NONE} means no |
|
1235 change. |
1235 |
1236 |
1236 \<^descr> \<^ML>\<open>Proof_Checker.thm_of_proof\<close>~\<open>thy prf\<close> turns the given (full) proof |
1237 \<^descr> \<^ML>\<open>Proof_Checker.thm_of_proof\<close>~\<open>thy prf\<close> turns the given (full) proof |
1237 into a theorem, by replaying it using only primitive rules of the inference |
1238 into a theorem, by replaying it using only primitive rules of the inference |
1238 kernel. |
1239 kernel. |
1239 |
1240 |