# HG changeset patch
# User lcp
# Date 775993559 -7200
# Node ID a00301e9e64bcc6fd3496b52ab4dbd4df1112f64
# Parent  e0ca460d6e518f241a31f12bad6280e5c07dee10
addition of show_brackets

diff -r e0ca460d6e51 -r a00301e9e64b doc-src/ERRATA.txt
--- a/doc-src/ERRATA.txt	Wed Aug 03 09:45:42 1994 +0200
+++ b/doc-src/ERRATA.txt	Thu Aug 04 11:45:59 1994 +0200
@@ -6,21 +6,20 @@
 
 *page 50: In section heading, Mixfix should be mixfix
 
-page 52: the declaration  "types bool,nat"  is illegal    
-
 *page 217 and 251: fst and snd should be fst_conv and snd_conv.
 *Also affects index: pages 310 and 317!
 
-pages 222, 223: The braces need escaping in
-\tdx{qconverse_def}   qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}
-\tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). {<x;y>}
-\tdx{lfp_def}        lfp(D,h) == Inter({X: Pow(D). h(X) <= X})
-\tdx{gfp_def}        gfp(D,h) == Union({X: Pow(D). X <= h(X)})
-
 *page 224: type of id, namely $\To i$, should be $i \To i$ 
 
-Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc]
-should be addsimps
+Intro/advanced
+page 52: the declaration  "types bool,nat"  is illegal    
+
+should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]'
+
+
+Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing}
+
+Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control}
 
 Ref/tactic: documented subgoals_tac
 
@@ -29,9 +28,12 @@
 Ref/defining: type constraints ("::") now have a very low priority of 4.
               As in ML, they must be enclosed in paretheses most of the time.
 
-Ref/syntax (page 145?): there is a repeated "the" in "before the the .thy file"
+Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file"
 
-Logics/ZF: renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
+Logics/ZF: ****************
+renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
 renamed union_iff to Union_iff
 renamed power_set to Pow_iff
 DiffD2: now is really a destruction rule
+escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def
+
diff -r e0ca460d6e51 -r a00301e9e64b doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Wed Aug 03 09:45:42 1994 +0200
+++ b/doc-src/Ref/goals.tex	Thu Aug 04 11:45:59 1994 +0200
@@ -190,13 +190,15 @@
   find no alternative proof state.
 \end{itemize}
 
-\subsection{Printing the proof state}
+\subsection{Printing the proof state}\label{sec:goals-printing}
 \index{proof state!printing of}
 \begin{ttbox} 
 pr    : unit -> unit
 prlev : int -> unit
 goals_limit: int ref \hfill{\bf initially 10}
 \end{ttbox}
+See also the printing control options described in
+\S\ref{sec:printing-control}. 
 \begin{ttdescription}
 \item[\ttindexbold{pr}();] 
 prints the current proof state.