1.1 --- a/doc-src/Logics/Old_HOL.tex Tue May 03 10:40:24 1994 +0200
1.2 +++ b/doc-src/Logics/Old_HOL.tex Tue May 03 10:52:32 1994 +0200
1.3 @@ -856,8 +856,8 @@
1.4
1.5
1.6 \tdx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
1.7 -\tdx{fst} fst(<a,b>) = a
1.8 -\tdx{snd} snd(<a,b>) = b
1.9 +\tdx{fst_conv} fst(<a,b>) = a
1.10 +\tdx{snd_conv} snd(<a,b>) = b
1.11 \tdx{split} split(<a,b>, c) = c(a,b)
1.12
1.13 \tdx{surjective_pairing} p = <fst(p),snd(p)>
2.1 --- a/doc-src/Logics/ZF.tex Tue May 03 10:40:24 1994 +0200
2.2 +++ b/doc-src/Logics/ZF.tex Tue May 03 10:52:32 1994 +0200
2.3 @@ -746,8 +746,8 @@
2.4 \tdx{Pair_inject} [| <a,b> = <c,d>; [| a=c; b=d |] ==> P |] ==> P
2.5 \tdx{Pair_neq_0} <a,b>=0 ==> P
2.6
2.7 -\tdx{fst} fst(<a,b>) = a
2.8 -\tdx{snd} snd(<a,b>) = b
2.9 +\tdx{fst_conv} fst(<a,b>) = a
2.10 +\tdx{snd_conv} snd(<a,b>) = b
2.11 \tdx{split} split(\%x y.c(x,y), <a,b>) = c(a,b)
2.12
2.13 \tdx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
2.14 @@ -1148,7 +1148,7 @@
2.15 \begin{constants}
2.16 \it symbol & \it meta-type & \it priority & \it description \\
2.17 \sdx{O} & $[i,i]\To i$ & Right 60 & composition ($\circ$) \\
2.18 - \cdx{id} & $\To i$ & & identity function \\
2.19 + \cdx{id} & $i\To i$ & & identity function \\
2.20 \cdx{inj} & $[i,i]\To i$ & & injective function space\\
2.21 \cdx{surj} & $[i,i]\To i$ & & surjective function space\\
2.22 \cdx{bij} & $[i,i]\To i$ & & bijective function space
3.1 --- a/doc-src/Logics/logics.tex Tue May 03 10:40:24 1994 +0200
3.2 +++ b/doc-src/Logics/logics.tex Tue May 03 10:52:32 1994 +0200
3.3 @@ -2,9 +2,9 @@
3.4 %% $Id$
3.5 %%%STILL NEEDS MODAL, LCF
3.6 %%%\includeonly{ZF}
3.7 -%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\idx{\1}
3.8 -%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\idx{\1}
3.9 -%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\idx{\1}
3.10 +%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
3.11 +%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
3.12 +%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
3.13 %%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
3.14 %% run ../sedindex logics to prepare index file
3.15 \title{Isabelle's Object-Logics}
3.16 @@ -16,7 +16,7 @@
3.17 Martin Coen made many contributions to~\ZF{}. Martin Coen
3.18 developed~\Modal{} with assistance from Rajeev Gor\'e. The research
3.19 has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT
3.20 - project 6453: Types}.\\
3.21 + project 6453: Types.}\\
3.22 Computer Laboratory \\
3.23 University of Cambridge \\[2ex]
3.24 {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
3.25 @@ -26,13 +26,10 @@
3.26
3.27 \newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
3.28 \hrule\bigskip}
3.29 +\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
3.30
3.31 \makeindex
3.32
3.33 -%For indexing names in ttbox; could be local to Chapters, making a subitem...
3.34 -\let\idx=\ttindexbold
3.35 -%%%%\newcommand\idx[1]{\indexbold{*#1}#1}
3.36 -
3.37 %%\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
3.38 %%\newtheorem{Example}{Example}[chapter]
3.39
3.40 @@ -57,6 +54,6 @@
3.41 %%\include{Cube}
3.42 %%\include{LCF}
3.43 \bibliographystyle{plain}
3.44 -\bibliography{atp,theory,funprog,logicprog,isabelle}
3.45 +\bibliography{string,atp,theory,funprog,logicprog,isabelle}
3.46 \input{logics.ind}
3.47 \end{document}
4.1 --- a/doc-src/Ref/ref.tex Tue May 03 10:40:24 1994 +0200
4.2 +++ b/doc-src/Ref/ref.tex Tue May 03 10:52:32 1994 +0200
4.3 @@ -1,23 +1,25 @@
4.4 \documentstyle[a4,12pt,rail,proof,iman,extra]{report}
4.5 %% $Id$
4.6 -%%% \includeonly{thm}
4.7 +%%\includeonly{}
4.8 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1}
4.9 %%% to delete old ones: \\indexbold{\*[^}]*}
4.10 %% run sedindex ref to prepare index file
4.11 %%% needs chapter on Provers/typedsimp.ML?
4.12 \title{The Isabelle Reference Manual}
4.13
4.14 -\author{{\em Lawrence C. Paulson}\thanks
4.15 -{Tobias Nipkow, of T. U. Munich, wrote Chapter~8 and part of Chapter~6.
4.16 - Carsten Clasohm also contributed to Chapter~6.
4.17 - Sara Kalvala and Markus Wenzel suggested changes and corrections.
4.18 - The research has been funded by the SERC (grants GR/G53279, GR/H40570)
4.19 - and by ESPRIT project 6453: Types.}
4.20 -\\
4.21 - Computer Laboratory \\ University of Cambridge \\[2ex]
4.22 - {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
4.23 - {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
4.24 -}
4.25 +\author{{\em Lawrence C. Paulson}%
4.26 +\thanks{Tobias Nipkow, of T. U. Munich, wrote most of
4.27 + Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of
4.28 + Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to
4.29 + Chapter~\protect\ref{theories}. Markus Wenzel contributed to
4.30 + Chapter~\protect\ref{chap:syntax}. Sara Kalvala and others suggested changes
4.31 + and corrections. The research has been funded by the SERC (grants
4.32 + GR/G53279, GR/H40570) and by ESPRIT project 6453: Types.}
4.33 +\\
4.34 +Computer Laboratory \\ University of Cambridge \\[2ex]
4.35 +\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}\\[3cm]
4.36 +Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
4.37 +
4.38 \date{}
4.39 \makeindex
4.40
4.41 @@ -54,8 +56,9 @@
4.42
4.43 \begingroup
4.44 \bibliographystyle{plain} \small\raggedright\frenchspacing
4.45 - \bibliography{atp,funprog,general,logicprog,theory}
4.46 + \bibliography{string,atp,funprog,general,logicprog,isabelle,theory}
4.47 \endgroup
4.48 \include{theory-syntax}
4.49 -\addcontentsline{toc}{chapter}{Index}\input{ref.ind}
4.50 +
4.51 +\input{ref.ind}
4.52 \end{document}