more on concrete syntax of proof terms;

--- a/src/Doc/IsarImplementation/Logic.thy	Mon Jun 17 20:15:34 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy	Mon Jun 17 21:23:49 2013 +0200
@@ -1291,6 +1291,46 @@
   and can turn it into a theorem by replaying its primitive inferences
   within the kernel.  *}
 
+
+subsection {* Concrete syntax of proof terms *}
+
+text {* The concrete syntax of proof terms is a slight extension of
+  the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}.
+  Its main syntactic category @{syntax (inner) proof} is defined as
+  follows:
+
+  \begin{center}
+  \begin{supertabular}{rclr}
+
+  @{syntax_def (inner) proof} & = & @{verbatim Lam} @{text params} @{verbatim "."} @{text proof} \\
+    & @{text "|"} & @{text "\<Lambda>"} @{text "params"} @{verbatim "."} @{text proof} \\
+    & @{text "|"} & @{text proof} @{verbatim "%"} @{text any} \\
+    & @{text "|"} & @{text proof} @{text "\<cdot>"} @{text any} \\
+    & @{text "|"} & @{text proof} @{verbatim "%%"} @{text proof} \\
+    & @{text "|"} & @{text proof} @{text "\<bullet>"} @{text proof} \\
+    & @{text "|"} & @{text "id  |  longid"} \\
+  \\
+
+  @{text param} & = & @{text idt} \\
+    & @{text "|"} & @{text idt} @{verbatim ":"} @{text prop} \\
+    & @{text "|"} & @{verbatim "("} @{text param} @{verbatim ")"} \\
+  \\
+
+  @{text params} & = & @{text param} \\
+    & @{text "|"} & @{text param} @{text params} \\
+
+  \end{supertabular}
+  \end{center}
+
+  Implicit term arguments in partial proofs are indicated by ``@{text
+  "_"}''.  Type arguments for theorems and axioms may be specified
+  using @{text "p \<cdot> TYPE(type)"} (they must appear before any other
+  term argument of a theorem or axiom, but may be omitted altogether).
+
+  \medskip There are separate read and print operations for proof
+  terms, in order to avoid conflicts with the regular term language.
+*}
+
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type proof} \\
@@ -1300,8 +1340,9 @@
   "theory -> term -> proof -> proof"} \\
   @{index_ML Reconstruct.expand_proof: "theory ->
   (string * term option) list -> proof -> proof"} \\
-  @{index_ML Proof_Checker.thm_of_proof:
-  "theory -> proof -> thm"} \\
+  @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
+  @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
+  @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
   \end{mldecls}
 
   \begin{description}
@@ -1354,6 +1395,14 @@
   given (full) proof into a theorem, by replaying it using only
   primitive rules of the inference kernel.
 
+  \item @{ML Proof_Syntax.read_proof}~@{text "thy b\<^sub>1 b\<^sub>2 s"} reads in a
+  proof term. The Boolean flags indicate the use of sort and type
+  information.  Usually, typing information is left implicit and is
+  inferred during proof reconstruction.  %FIXME eliminate flags!?
+
+  \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}
+  pretty-prints the given proof term.
+
   \end{description}
 *}
 
@@ -1434,12 +1483,11 @@
          pretty_item "full proof:"
           (Proof_Syntax.pretty_proof ctxt full_prf)]
         |> Pretty.chunks |> Pretty.writeln;
-
+    in
       (*rechecked theorem*)
-      val thm' =
-        Proof_Checker.thm_of_proof thy full_prf
-        |> singleton (Proof_Context.export ctxt ctxt0);
-    in thm' end;
+      Proof_Checker.thm_of_proof thy full_prf
+      |> singleton (Proof_Context.export ctxt ctxt0)
+    end;
 *}
 
 text {* As anticipated, the rechecked theorem establishes the same

--- a/src/Doc/IsarImplementation/document/root.tex	Mon Jun 17 20:15:34 2013 +0200
+++ b/src/Doc/IsarImplementation/document/root.tex	Mon Jun 17 21:23:49 2013 +0200
@@ -7,6 +7,7 @@
 \usepackage{isabellesym}
 \usepackage{railsetup}
 \usepackage{ttbox}
+\usepackage{supertabular}
 \usepackage{style}
 \usepackage{pdfsetup}
 
@@ -19,6 +20,7 @@
   \\[4ex] The Isabelle/Isar Implementation}
 \author{\emph{Makarius Wenzel}  \\[3ex]
   With Contributions by
+  Stefan Berghofer, \\
   Florian Haftmann
   and Larry Paulson
 }

--- a/src/Doc/ROOT	Mon Jun 17 20:15:34 2013 +0200
+++ b/src/Doc/ROOT	Mon Jun 17 21:23:49 2013 +0200
@@ -258,7 +258,6 @@
     "document/build"
     "document/root.tex"
     "document/syntax.tex"
-    "document/thm.tex"
 
 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   options [document_variants = "sledgehammer"]

--- a/src/Doc/Ref/document/root.tex	Mon Jun 17 20:15:34 2013 +0200
+++ b/src/Doc/Ref/document/root.tex	Mon Jun 17 21:23:49 2013 +0200
@@ -41,7 +41,6 @@
 
 \pagenumbering{roman} \tableofcontents \clearfirst
 
-\input{thm}
 \input{syntax}
 
 %%seealso's must be last so that they appear last in the index entries

--- a/src/Doc/Ref/document/thm.tex	Mon Jun 17 20:15:34 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-
-\chapter{Theorems and Forward Proof}
-
-\section{Proof terms}\label{sec:proofObjects}
-
-
-\subsection{Parsing and printing proof terms}
-\index{proof terms!parsing}
-\index{proof terms!printing}
-
-Isabelle offers several functions for parsing and printing
-proof terms. The concrete syntax for proof terms is described
-in Fig.\ts\ref{fig:proof_gram}.
-Implicit term arguments in partial proofs are indicated
-by ``{\tt _}''.
-Type arguments for theorems and axioms may be specified using
-\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)}
-(see \S\ref{sec:basic_syntax}).
-They must appear before any other term argument of a theorem
-or axiom. In contrast to term arguments, type arguments may
-be completely omitted.
-\begin{ttbox}
-ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof
-ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
-ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T
-ProofSyntax.print_proof_of : bool -> thm -> unit
-\end{ttbox}
-\begin{figure}
-\begin{center}
-\begin{tabular}{rcl}
-$proof$  & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~
-                 $\Lambda params${\tt .} $proof$ \\
-         & $|$ & $proof$ \verb!%! $any$ ~~$|$~~
-                 $proof$ $\cdot$ $any$ \\
-         & $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~
-                 $proof$ {\boldmath$\cdot$} $proof$ \\
-         & $|$ & $id$ ~~$|$~~ $longid$ \\\\
-$param$  & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~
-                 {\tt (} $param$ {\tt )} \\\\
-$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$
-\end{tabular}
-\end{center}
-\caption{Proof term syntax}\label{fig:proof_gram}
-\end{figure}
-The function {\tt read_proof} reads in a proof term with
-respect to a given theory. The boolean flag indicates whether
-the proof term to be parsed contains explicit typing information
-to be taken into account.
-Usually, typing information is left implicit and
-is inferred during proof reconstruction. The pretty printing
-functions operating on theorems take a boolean flag as an
-argument which indicates whether the proof term should
-be reconstructed before printing.
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End: