# 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= & z=} -\tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {} -\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.