--- a/src/Doc/IsarImplementation/Logic.thy Thu Jun 27 20:09:39 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Thu Jun 27 23:17:26 2013 +0200
@@ -1335,7 +1335,6 @@
\begin{mldecls}
@{index_ML_type proof} \\
@{index_ML_type proof_body} \\
- @{index_ML proofs: "int Unsynchronized.ref"} \\
@{index_ML Reconstruct.reconstruct_proof:
"theory -> term -> proof -> proof"} \\
@{index_ML Reconstruct.expand_proof: "theory ->
@@ -1345,6 +1344,10 @@
@{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
\end{mldecls}
+ \begin{tabular}{rcll}
+ @{attribute_def proofs} & : & @{text attribute} & default @{text 1} \\
+ \end{tabular}
+
\begin{description}
\item Type @{ML_type proof} represents proof terms; this is a
@@ -1370,13 +1373,6 @@
Parallel performance may suffer by inspecting proof terms at
run-time.
- \item @{ML proofs} specifies the detail of proof recording within
- @{ML_type thm} values produced by the inference kernel: @{ML 0}
- records only the names of oracles, @{ML 1} records oracle names and
- propositions, @{ML 2} additionally records full proof terms.
- Officially named theorems that contribute to a result are recorded
- in any case.
-
\item @{ML Reconstruct.reconstruct_proof}~@{text "thy prop prf"}
turns the implicit proof term @{text "prf"} into a full proof of the
given proposition.
@@ -1404,6 +1400,13 @@
\item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}
pretty-prints the given proof term.
+ \item @{attribute proofs} specifies the detail of proof recording within
+ @{ML_type thm} values produced by the inference kernel: @{text 0}
+ records only the names of oracles, @{text 1} records oracle names and
+ propositions, @{text 2} additionally records full proof terms.
+ Officially named theorems that contribute to a result are recorded
+ in any case. %FIXME move to IsarRef
+
\end{description}
*}