src/Doc/Implementation/Logic.thy
changeset 65446 ed18feb34c07
parent 63680 6e1e8b5abbfa
child 67146 909dcdec2122
     1.1 --- a/src/Doc/Implementation/Logic.thy	Sat Apr 08 22:36:32 2017 +0200
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Sun Apr 09 19:03:55 2017 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    For \<open>k = 1\<close> the parentheses are omitted, e.g.\ \<open>\<alpha> list\<close> instead of
     1.5    \<open>(\<alpha>)list\<close>. Further notation is provided for specific constructors, notably
     1.6    the right-associative infix \<open>\<alpha> \<Rightarrow> \<beta>\<close> instead of \<open>(\<alpha>, \<beta>)fun\<close>.
     1.7 -  
     1.8 +
     1.9    The logical category \<^emph>\<open>type\<close> is defined inductively over type variables and
    1.10    type constructors as follows: \<open>\<tau> = \<alpha>\<^sub>s | ?\<alpha>\<^sub>s | (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>\<close>.
    1.11  
    1.12 @@ -1186,7 +1186,7 @@
    1.13    \begin{mldecls}
    1.14    @{index_ML_type proof} \\
    1.15    @{index_ML_type proof_body} \\
    1.16 -  @{index_ML proofs: "int Unsynchronized.ref"} \\
    1.17 +  @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
    1.18    @{index_ML Reconstruct.reconstruct_proof:
    1.19    "Proof.context -> term -> proof -> proof"} \\
    1.20    @{index_ML Reconstruct.expand_proof: "Proof.context ->
    1.21 @@ -1215,11 +1215,11 @@
    1.22    construction of proofs by introducing dynamic ad-hoc dependencies. Parallel
    1.23    performance may suffer by inspecting proof terms at run-time.
    1.24  
    1.25 -  \<^descr> @{ML proofs} specifies the detail of proof recording within @{ML_type thm}
    1.26 -  values produced by the inference kernel: @{ML 0} records only the names of
    1.27 -  oracles, @{ML 1} records oracle names and propositions, @{ML 2} additionally
    1.28 -  records full proof terms. Officially named theorems that contribute to a
    1.29 -  result are recorded in any case.
    1.30 +  \<^descr> @{ML Proofterm.proofs} specifies the detail of proof recording within
    1.31 +  @{ML_type thm} values produced by the inference kernel: @{ML 0} records only
    1.32 +  the names of oracles, @{ML 1} records oracle names and propositions, @{ML 2}
    1.33 +  additionally records full proof terms. Officially named theorems that
    1.34 +  contribute to a result are recorded in any case.
    1.35  
    1.36    \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>ctxt prop prf\<close> turns the implicit
    1.37    proof term \<open>prf\<close> into a full proof of the given proposition.