1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Sat Jun 15 16:55:49 2013 +0200
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Sat Jun 15 21:01:07 2013 +0200
     1.3 @@ -378,8 +378,9 @@
     1.4  
     1.5    \item Type @{ML_type term} represents de-Bruijn terms, with comments
     1.6    in abstractions, and explicitly named free variables and constants;
     1.7 -  this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
     1.8 -  Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}.
     1.9 +  this is a datatype with constructors @{index_ML Bound}, @{index_ML
    1.10 +  Free}, @{index_ML Var}, @{index_ML Const}, @{index_ML Abs},
    1.11 +  @{index_ML_op "$"}.
    1.12  
    1.13    \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
    1.14    "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
    1.15 @@ -554,10 +555,10 @@
    1.16    "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
    1.17    are irrelevant in the Pure logic, though; they cannot occur within
    1.18    propositions.  The system provides a runtime option to record
    1.19 -  explicit proof terms for primitive inferences.  Thus all three
    1.20 -  levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
    1.21 -  terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
    1.22 -  \cite{Berghofer-Nipkow:2000:TPHOL}).
    1.23 +  explicit proof terms for primitive inferences, see also
    1.24 +  \secref{sec:proof-terms}.  Thus all three levels of @{text
    1.25 +  "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for terms, and @{text
    1.26 +  "\<And>/\<Longrightarrow>"} for proofs (cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}).
    1.27  
    1.28    Observe that locally fixed parameters (as in @{text
    1.29    "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
    1.30 @@ -647,7 +648,6 @@
    1.31    \end{mldecls}
    1.32    \begin{mldecls}
    1.33    @{index_ML_type thm} \\
    1.34 -  @{index_ML proofs: "int Unsynchronized.ref"} \\
    1.35    @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
    1.36    @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
    1.37    @{index_ML Thm.assume: "cterm -> thm"} \\
    1.38 @@ -721,12 +721,6 @@
    1.39    Every @{ML_type thm} value contains a sliding back-reference to the
    1.40    enclosing theory, cf.\ \secref{sec:context-theory}.
    1.41  
    1.42 -  \item @{ML proofs} specifies the detail of proof recording within
    1.43 -  @{ML_type thm} values: @{ML 0} records only the names of oracles,
    1.44 -  @{ML 1} records oracle names and propositions, @{ML 2} additionally
    1.45 -  records full proof terms.  Officially named theorems that contribute
    1.46 -  to a result are recorded in any case.
    1.47 -
    1.48    \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given
    1.49    theorem to a \emph{larger} theory, see also \secref{sec:context}.
    1.50    This formal adjustment of the background context has no logical
    1.51 @@ -1279,4 +1273,45 @@
    1.52    without the full overhead of explicit proof terms.
    1.53  *}
    1.54  
    1.55 +text %mlref {*
    1.56 +  \begin{mldecls}
    1.57 +  @{index_ML_type proof} \\
    1.58 +  @{index_ML_type proof_body} \\
    1.59 +  @{index_ML proofs: "int Unsynchronized.ref"} \\
    1.60 +  \end{mldecls}
    1.61 +
    1.62 +  \begin{description}
    1.63 +
    1.64 +  \item Type @{ML_type proof} represents proof terms; this is a
    1.65 +  datatype with constructors @{index_ML Abst}, @{index_ML AbsP},
    1.66 +  @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},
    1.67 +  @{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML
    1.68 +  Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.
    1.69 +
    1.70 +  \item Type @{ML_type proof_body} represents the nested proof
    1.71 +  information of a named theorem, consisting of a digest of oracles
    1.72 +  and named theorem over some proof term.  The digest only covers the
    1.73 +  directly visible part of the proof: in order to get the full
    1.74 +  information, the implicit graph of nested theorems needs to be
    1.75 +  traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).
    1.76 +
    1.77 +  \item @{ML Thm.proof_of}~@{text "thm"} and @{ML
    1.78 +  Thm.proof_body_of}~@{text "thm"} produce the proof term or proof
    1.79 +  body (with digest of oracles and theorems) from a given theorem.
    1.80 +  Note that this involves a full join of internal futures that fulfill
    1.81 +  pending proof promises, and thus disrupts the natural bottom-up
    1.82 +  construction of proofs by introducing dynamic ad-hoc dependencies.
    1.83 +  Parallel performance may suffer by inspecting proof terms at
    1.84 +  run-time.
    1.85 +
    1.86 +  \item @{ML proofs} specifies the detail of proof recording within
    1.87 +  @{ML_type thm} values produced by the inference kernel: @{ML 0}
    1.88 +  records only the names of oracles, @{ML 1} records oracle names and
    1.89 +  propositions, @{ML 2} additionally records full proof terms.
    1.90 +  Officially named theorems that contribute to a result are recorded
    1.91 +  in any case.
    1.92 +
    1.93 +  \end{description}
    1.94 +*}
    1.95 +
    1.96  end

     2.1 --- a/src/Doc/Ref/document/thm.tex	Sat Jun 15 16:55:49 2013 +0200
     2.2 +++ b/src/Doc/Ref/document/thm.tex	Sat Jun 15 21:01:07 2013 +0200
     2.3 @@ -2,58 +2,7 @@
     2.4  \chapter{Theorems and Forward Proof}
     2.5  
     2.6  \section{Proof terms}\label{sec:proofObjects}
     2.7 -\begin{ttbox}
     2.8 -infix 8 % %%;
     2.9  
    2.10 -datatype proof =
    2.11 -   PBound of int
    2.12 - | Abst of string * typ option * proof
    2.13 - | AbsP of string * term option * proof
    2.14 - | op % of proof * term option
    2.15 - | op %% of proof * proof
    2.16 - | Hyp of term
    2.17 - | PThm of (string * (string * string list) list) *
    2.18 -           proof * term * typ list option
    2.19 - | PAxm of string * term * typ list option
    2.20 - | Oracle of string * term * typ list option
    2.21 - | MinProof of proof list;
    2.22 -\end{ttbox}
    2.23 -
    2.24 -\begin{ttdescription}
    2.25 -\item[\ttindexbold{Abst} ($a$, $\tau$, $prf$)] is the abstraction over
    2.26 -a {\it term variable} of type $\tau$ in the body $prf$. Logically, this
    2.27 -corresponds to $\bigwedge$ introduction. The name $a$ is used only for
    2.28 -parsing and printing.
    2.29 -\item[\ttindexbold{AbsP} ($a$, $\varphi$, $prf$)] is the abstraction
    2.30 -over a {\it proof variable} standing for a proof of proposition $\varphi$
    2.31 -in the body $prf$. This corresponds to $\Longrightarrow$ introduction.
    2.32 -\item[$prf$ \% $t$] \index{\%@{\tt\%}|bold}
    2.33 -is the application of proof $prf$ to term $t$
    2.34 -which corresponds to $\bigwedge$ elimination.
    2.35 -\item[$prf@1$ \%\% $prf@2$] \index{\%\%@{\tt\%\%}|bold}
    2.36 -is the application of proof $prf@1$ to
    2.37 -proof $prf@2$ which corresponds to $\Longrightarrow$ elimination.
    2.38 -\item[\ttindexbold{PBound} $i$] is a {\em proof variable} with de Bruijn
    2.39 -\cite{debruijn72} index $i$.
    2.40 -\item[\ttindexbold{Hyp} $\varphi$] corresponds to the use of a meta level
    2.41 -hypothesis $\varphi$.
    2.42 -\item[\ttindexbold{PThm} (($name$, $tags$), $prf$, $\varphi$, $\overline{\tau}$)]
    2.43 -stands for a pre-proved theorem, where $name$ is the name of the theorem,
    2.44 -$prf$ is its actual proof, $\varphi$ is the proven proposition,
    2.45 -and $\overline{\tau}$ is
    2.46 -a type assignment for the type variables occurring in the proposition.
    2.47 -\item[\ttindexbold{PAxm} ($name$, $\varphi$, $\overline{\tau}$)]
    2.48 -corresponds to the use of an axiom with name $name$ and proposition
    2.49 -$\varphi$, where $\overline{\tau}$ is a type assignment for the type
    2.50 -variables occurring in the proposition.
    2.51 -\item[\ttindexbold{Oracle} ($name$, $\varphi$, $\overline{\tau}$)]
    2.52 -denotes the invocation of an oracle with name $name$ which produced
    2.53 -a proposition $\varphi$, where $\overline{\tau}$ is a type assignment
    2.54 -for the type variables occurring in the proposition.
    2.55 -\item[\ttindexbold{MinProof} $prfs$]
    2.56 -represents a {\em minimal proof} where $prfs$ is a list of theorems,
    2.57 -axioms or oracles.
    2.58 -\end{ttdescription}
    2.59  Note that there are no separate constructors
    2.60  for abstraction and application on the level of {\em types}, since
    2.61  instantiation of type variables is accomplished via the type assignments
    2.62 @@ -73,15 +22,6 @@
    2.63  The theorem is applied to two (implicit) term arguments, which correspond
    2.64  to the two variables occurring in its proposition.
    2.65  
    2.66 -Isabelle's inference kernel can produce proof objects with different
    2.67 -levels of detail. This is controlled via the global reference variable
    2.68 -\ttindexbold{proofs}:
    2.69 -\begin{ttdescription}
    2.70 -\item[proofs := 0;] only record uses of oracles
    2.71 -\item[proofs := 1;] record uses of oracles as well as dependencies
    2.72 -  on other theorems and axioms
    2.73 -\item[proofs := 2;] record inferences in full detail
    2.74 -\end{ttdescription}
    2.75  Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs}
    2.76  will not work for proofs constructed with {\tt proofs} set to
    2.77  {\tt 0} or {\tt 1}.

     3.1 --- a/src/Doc/antiquote_setup.ML	Sat Jun 15 16:55:49 2013 +0200
     3.2 +++ b/src/Doc/antiquote_setup.ML	Sat Jun 15 21:01:07 2013 +0200
     3.3 @@ -19,6 +19,8 @@
     3.4  val clean_string = translate
     3.5    (fn "_" => "\\_"
     3.6      | "#" => "\\#"
     3.7 +    | "$" => "\\$"
     3.8 +    | "%" => "\\%"
     3.9      | "<" => "$<$"
    3.10      | ">" => "$>$"
    3.11      | "{" => "\\{"