# HG changeset patch # User lcp # Date 767955152 -7200 # Node ID 0ddc495e8b83308f4600f0c9f23ba02d9df143ee # Parent 1f5a94209c972c176a14d6a22d3d3eb15ac0270e post-CRC corrections diff -r 1f5a94209c97 -r 0ddc495e8b83 doc-src/Logics/Old_HOL.tex --- 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=a'; b=b' |] ==> R |] ==> R -\tdx{fst} fst() = a -\tdx{snd} snd() = b +\tdx{fst_conv} fst() = a +\tdx{snd_conv} snd() = b \tdx{split} split(, c) = c(a,b) \tdx{surjective_pairing} p = diff -r 1f5a94209c97 -r 0ddc495e8b83 doc-src/Logics/ZF.tex --- 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=c; b=d |] ==> P |] ==> P \tdx{Pair_neq_0} =0 ==> P -\tdx{fst} fst() = a -\tdx{snd} snd() = b +\tdx{fst_conv} fst() = a +\tdx{snd_conv} snd() = b \tdx{split} split(\%x y.c(x,y), ) = c(a,b) \tdx{SigmaI} [| a:A; b:B(a) |] ==> : 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 diff -r 1f5a94209c97 -r 0ddc495e8b83 doc-src/Logics/logics.tex --- 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 lcp@cl.cam.ac.uk}} \\[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} diff -r 1f5a94209c97 -r 0ddc495e8b83 doc-src/Ref/ref.tex --- 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 lcp@cl.cam.ac.uk}} \\[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 lcp@cl.cam.ac.uk}\\[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}