post-CRC corrections

--- a/doc-src/Logics/Old_HOL.tex	Tue May 03 10:40:24 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Tue May 03 10:52:32 1994 +0200
@@ -856,8 +856,8 @@
 
 
 \tdx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
-\tdx{fst}          fst(<a,b>) = a
-\tdx{snd}          snd(<a,b>) = b
+\tdx{fst_conv}     fst(<a,b>) = a
+\tdx{snd_conv}     snd(<a,b>) = b
 \tdx{split}        split(<a,b>, c) = c(a,b)
 
 \tdx{surjective_pairing}  p = <fst(p),snd(p)>

--- a/doc-src/Logics/ZF.tex	Tue May 03 10:40:24 1994 +0200
+++ b/doc-src/Logics/ZF.tex	Tue May 03 10:52:32 1994 +0200
@@ -746,8 +746,8 @@
 \tdx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
 \tdx{Pair_neq_0}      <a,b>=0 ==> P
 
-\tdx{fst}             fst(<a,b>) = a
-\tdx{snd}             snd(<a,b>) = b
+\tdx{fst_conv}        fst(<a,b>) = a
+\tdx{snd_conv}        snd(<a,b>) = b
 \tdx{split}           split(\%x y.c(x,y), <a,b>) = c(a,b)
 
 \tdx{SigmaI}          [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
@@ -1148,7 +1148,7 @@
 \begin{constants} 
   \it symbol  & \it meta-type & \it priority & \it description \\ 
   \sdx{O}       & $[i,i]\To i$  &  Right 60     & composition ($\circ$) \\
-  \cdx{id}      & $\To i$       &       & identity function \\
+  \cdx{id}      & $i\To i$      &       & identity function \\
   \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
   \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
   \cdx{bij}     & $[i,i]\To i$  &       & bijective function space

--- a/doc-src/Logics/logics.tex	Tue May 03 10:40:24 1994 +0200
+++ b/doc-src/Logics/logics.tex	Tue May 03 10:52:32 1994 +0200
@@ -2,9 +2,9 @@
 %% $Id$
 %%%STILL NEEDS MODAL, LCF
 %%%\includeonly{ZF}
-%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\idx{\1}  
-%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\idx{\1}  
-%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\idx{\1}  
+%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
+%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
+%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
 %%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
 %% run    ../sedindex logics    to prepare index file
 \title{Isabelle's Object-Logics}
@@ -16,7 +16,7 @@
     Martin Coen made many contributions to~\ZF{}.  Martin Coen
     developed~\Modal{} with assistance from Rajeev Gor\'e.  The research
     has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT
-    project 6453: Types}.\\ 
+    project 6453: Types.}\\ 
   Computer Laboratory \\ 
   University of Cambridge \\[2ex] 
   {\small{\em Electronic mail\/}: {\tt [e-mail]}} \\[3cm]
@@ -26,13 +26,10 @@
 
 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
   \hrule\bigskip}
+\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
 
 \makeindex
 
-%For indexing names in ttbox; could be local to Chapters, making a subitem...
-\let\idx=\ttindexbold
-%%%%\newcommand\idx[1]{\indexbold{*#1}#1}
-
 %%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
 %%\newtheorem{Example}{Example}[chapter]
 
@@ -57,6 +54,6 @@
 %%\include{Cube}
 %%\include{LCF}
 \bibliographystyle{plain}
-\bibliography{atp,theory,funprog,logicprog,isabelle}
+\bibliography{string,atp,theory,funprog,logicprog,isabelle}
 \input{logics.ind}
 \end{document}

--- a/doc-src/Ref/ref.tex	Tue May 03 10:40:24 1994 +0200
+++ b/doc-src/Ref/ref.tex	Tue May 03 10:52:32 1994 +0200
@@ -1,23 +1,25 @@
 \documentstyle[a4,12pt,rail,proof,iman,extra]{report}
 %% $Id$
-%%% \includeonly{thm}
+%%\includeonly{}
 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
 %%% to delete old ones:  \\indexbold{\*[^}]*}
 %% run    sedindex ref    to prepare index file
 %%% needs chapter on Provers/typedsimp.ML?
 \title{The Isabelle Reference Manual}
 
-\author{{\em Lawrence C. Paulson}\thanks
-{Tobias Nipkow, of T. U. Munich, wrote Chapter~8 and part of Chapter~6.
- Carsten Clasohm also contributed to Chapter~6.
- Sara Kalvala and Markus Wenzel suggested changes and corrections.
- The research has been funded by the SERC (grants GR/G53279, GR/H40570)
-  and by ESPRIT project 6453: Types.} 
-\\  
-        Computer Laboratory \\ University of Cambridge \\[2ex]
-        {\small{\em Electronic mail\/}: {\tt [e-mail]}} \\[3cm]
-    {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
-}
+\author{{\em Lawrence C. Paulson}%
+\thanks{Tobias Nipkow, of T. U. Munich, wrote most of
+  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of
+  Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
+  Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
+  Chapter~\protect\ref{chap:syntax}.  Sara Kalvala and others suggested changes
+  and corrections.  The research has been funded by the SERC (grants
+  GR/G53279, GR/H40570) and by ESPRIT project 6453: Types.}
+\\
+Computer Laboratory \\ University of Cambridge \\[2ex] 
+\small{\em Electronic mail\/}: {\tt [e-mail]}\\[3cm]
+Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
+
 \date{} 
 \makeindex
 
@@ -54,8 +56,9 @@
 
 \begingroup
   \bibliographystyle{plain} \small\raggedright\frenchspacing
-  \bibliography{atp,funprog,general,logicprog,theory}
+  \bibliography{string,atp,funprog,general,logicprog,isabelle,theory}
 \endgroup
 \include{theory-syntax}
-\addcontentsline{toc}{chapter}{Index}\input{ref.ind}
+
+\input{ref.ind}
 \end{document}