# HG changeset patch
# User berghofe
# Date 1001696137 -7200
# Node ID 74cdf24724ea5a95264880d596661b58c619e8b5
# Parent  8a45c7abef0406dd314cf153386ef23458b9ed7e
Tuned section about parsing and printing proof terms.

diff -r 8a45c7abef04 -r 74cdf24724ea doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Fri Sep 28 17:19:46 2001 +0200
+++ b/doc-src/Ref/thm.tex	Fri Sep 28 18:55:37 2001 +0200
@@ -947,10 +947,10 @@
 or axiom. In contrast to term arguments, type arguments may
 be completely omitted.
 \begin{ttbox}
-  val read_proof : theory -> bool -> string -> Proofterm.proof
-  val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
-  val pretty_proof_of : bool -> thm -> Pretty.T
-  val print_proof_of : bool -> thm -> unit
+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}