first draft of Springer volume
authorlcp
Wed Mar 23 13:05:12 1994 +0100 (1994-03-23)
changeset 29363a0077dd9f2
parent 292 cc69ef31cfc3
child 294 058343877e3a
first draft of Springer volume
doc-src/iman.sty
doc-src/ind-defs.bbl
     1.1 --- a/doc-src/iman.sty	Wed Mar 23 11:32:21 1994 +0100
     1.2 +++ b/doc-src/iman.sty	Wed Mar 23 13:05:12 1994 +0100
     1.3 @@ -1,14 +1,16 @@
     1.4 -\typeout{Isabelle Manual Page Layout}
     1.5 -
     1.6 -% iman.sty 
     1.7 +% iman.sty : Isabelle Manual Page Layout
     1.8  %
     1.9 -\typeout{Document Style iman. Released 15 September 1992}
    1.10 +\typeout{Document Style iman. Released 17 February 1994}
    1.11  
    1.12 -\hyphenation{Isa-belle}
    1.13 +\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
    1.14 +\hyphenation{data-type data-types co-data-type co-data-types }
    1.15 +
    1.16 +\let\ts=\thinspace
    1.17  
    1.18  %%%INDEXING  use sedindex to process the index
    1.19  %index, putting page numbers of definitions in boldface
    1.20  \newcommand\bold[1]{{\bf#1}}
    1.21 +\newcommand\fnote[1]{#1n}
    1.22  \newcommand\indexbold[1]{\index{#1|bold}}
    1.23  
    1.24  %for cross-references: 2nd argument (page number) is ignored
    1.25 @@ -23,12 +25,6 @@
    1.26  \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
    1.27  
    1.28  
    1.29 -%%Euro-style date: 20 September 1955
    1.30 -\def\today{\number\day\space\ifcase\month\or
    1.31 -January\or February\or March\or April\or May\or June\or
    1.32 -July\or August\or September\or October\or November\or December\fi
    1.33 -\space\number\year}
    1.34 -
    1.35  %%% underscores as ordinary characters, not for subscripting
    1.36  %%  use @ or \sb for subscripting; use \at for @
    1.37  %%  only works in \tt font
    1.38 @@ -57,10 +53,10 @@
    1.39  %%%% ``WARNING'' environment
    1.40  \def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
    1.41  \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
    1.42 -  	 \baselineskip=0.9\baselineskip
    1.43 -	 \noindent \hangindent\parindent \hangafter=-2 
    1.44 -  	 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
    1.45 -	{\par\endgroup\medbreak}
    1.46 +         \small %%WAS\baselineskip=0.9\baselineskip
    1.47 +         \noindent \hangindent\parindent \hangafter=-2 
    1.48 +         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
    1.49 +        {\par\endgroup\medbreak}
    1.50  
    1.51  
    1.52  %%%% Standard logical symbols
    1.53 @@ -69,13 +65,10 @@
    1.54  \let\disj=\vee
    1.55  \let\imp=\rightarrow
    1.56  \let\bimp=\leftrightarrow
    1.57 -\newcommand\all[1]{\forall#1.}	%quantification
    1.58 +\newcommand\all[1]{\forall#1.}  %quantification
    1.59  \newcommand\ex[1]{\exists#1.}
    1.60  \newcommand{\pair}[1]{\langle#1\rangle}
    1.61  
    1.62 -\newenvironment{example}{\begin{Example}\rm}{\end{Example}}
    1.63 -\newtheorem{Example}{Example}[chapter]
    1.64 -
    1.65  \newcommand\lbrakk{\mathopen{[\![}}
    1.66  \newcommand\rbrakk{\mathclose{]\!]}}
    1.67  \newcommand\List[1]{\lbrakk#1\rbrakk}  %was \obj
    1.68 @@ -86,9 +79,6 @@
    1.69  \let\inter=\bigcap
    1.70  \let\union=\bigcup
    1.71  
    1.72 -\newcommand{\rew}{\mathop{\longrightarrow}}
    1.73 -\newcommand{\rewer}{\mathop{\longleftrightarrow}}
    1.74 -
    1.75  \def\ML{{\sc ml}}
    1.76  \def\OBJ{{\sc obj}}
    1.77  
    1.78 @@ -110,40 +100,16 @@
    1.79  \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
    1.80  \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
    1.81  
    1.82 -\chardef\ttilde=`\~  	% A tilde for \tt font
    1.83 -\chardef\ttback=`\\  	% A backslash for \tt font
    1.84 -\chardef\ttlbrace=`\{ 	% A left brace for \tt font
    1.85 -\chardef\ttrbrace=`\} 	% A right brace for \tt font
    1.86 +\chardef\ttilde=`\~     % A tilde for \tt font
    1.87 +\chardef\ttback=`\\     % A backslash for \tt font
    1.88 +\chardef\ttlbrace=`\{   % A left brace for \tt font
    1.89 +\chardef\ttrbrace=`\}   % A right brace for \tt font
    1.90  
    1.91  \newfont{\sltt}{cmsltt10}     %% for output from terminal sessions
    1.92  \newcommand\out{\ \sltt}
    1.93  
    1.94 -%Indented, boxed alltt environment; uses \small\tt font
    1.95 -%\leftmargini is LaTeX's first-level indentation for items (2.5em)
    1.96 -%@endparenv is LaTeX's trick for preventing indentation of next paragraph
    1.97 -\newenvironment{ttbox}{\par\nobreak\vskip-2pt
    1.98 -	   \vbox\bgroup \small\begin{alltt} \leftskip\leftmargini}%
    1.99 -	{\end{alltt}\egroup\vskip-7pt\@endparenv}
   1.100 -\newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}}
   1.101 -
   1.102 -
   1.103 -%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
   1.104 -\newcommand\clearfirst{\clearpage\ifodd\c@page\else
   1.105 -    \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
   1.106 -    \pagenumbering{arabic}}
   1.107 -
   1.108 -%%%Ruled chapter headings 
   1.109 -\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf 
   1.110 -   #1 \vskip 14pt\hrule height1pt}
   1.111 -\def\@makechapterhead#1{ { \parindent 0pt 
   1.112 - \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par 
   1.113 - \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
   1.114 -
   1.115 -\def\@makeschapterhead#1{ { \parindent 0pt \raggedright 
   1.116 - \@rulehead{#1} \par \nobreak \vskip 40pt } }
   1.117 -
   1.118  % "itmath.sty" use cmr italic for letters in math mode and get the
   1.119 -%	       usual letter spacing of text mode.
   1.120 +%              usual letter spacing of text mode.
   1.121  %
   1.122  % Michael Lawley, April 1993
   1.123  % (lawley@cit.gu.edu.au)
   1.124 @@ -178,4 +144,4 @@
   1.125  \@setmcodes{`a}{`z}{"7\@tempa 61}
   1.126  
   1.127  \ifx\define@mathgroup\undefined\else
   1.128 -	\define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi
   1.129 +        \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi
     2.1 --- a/doc-src/ind-defs.bbl	Wed Mar 23 11:32:21 1994 +0100
     2.2 +++ b/doc-src/ind-defs.bbl	Wed Mar 23 13:05:12 1994 +0100
     2.3 @@ -1,105 +1,143 @@
     2.4  \begin{thebibliography}{10}
     2.5  
     2.6  \bibitem{abramsky90}
     2.7 -Samson Abramsky.
     2.8 -\newblock The lazy lambda calculus.
     2.9 -\newblock In David~A. Turner, editor, {\em Resesarch Topics in Functional
    2.10 -  Programming}, pages 65--116. Addison-Wesley, 1977.
    2.11 +Abramsky, S.,
    2.12 +\newblock The lazy lambda calculus,
    2.13 +\newblock In {\em Resesarch Topics in Functional Programming}, D.~A. Turner,
    2.14 +  Ed. Addison-Wesley, 1977, pp.~65--116
    2.15  
    2.16  \bibitem{aczel77}
    2.17 -Peter Aczel.
    2.18 -\newblock An introduction to inductive definitions.
    2.19 -\newblock In J.~Barwise, editor, {\em Handbook of Mathematical Logic}, pages
    2.20 -  739--782. North-Holland, 1977.
    2.21 +Aczel, P.,
    2.22 +\newblock An introduction to inductive definitions,
    2.23 +\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
    2.24 +  North-Holland, 1977, pp.~739--782
    2.25  
    2.26  \bibitem{aczel88}
    2.27 -Peter Aczel.
    2.28 -\newblock {\em Non-Well-Founded Sets}.
    2.29 -\newblock CSLI, 1988.
    2.30 +Aczel, P.,
    2.31 +\newblock {\em Non-Well-Founded Sets},
    2.32 +\newblock CSLI, 1988
    2.33  
    2.34  \bibitem{bm79}
    2.35 -Robert~S. Boyer and J~Strother Moore.
    2.36 -\newblock {\em A Computational Logic}.
    2.37 -\newblock Academic Press, 1979.
    2.38 +Boyer, R.~S., Moore, J.~S.,
    2.39 +\newblock {\em A Computational Logic},
    2.40 +\newblock Academic Press, 1979
    2.41  
    2.42  \bibitem{camilleri92}
    2.43 -J.~Camilleri and T.~F. Melham.
    2.44 +Camilleri, J., Melham, T.~F.,
    2.45  \newblock Reasoning with inductively defined relations in the {HOL} theorem
    2.46 -  prover.
    2.47 -\newblock Technical Report 265, University of Cambridge Computer Laboratory,
    2.48 -  August 1992.
    2.49 +  prover,
    2.50 +\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, August 1992
    2.51  
    2.52  \bibitem{davey&priestley}
    2.53 -B.~A. Davey and H.~A. Priestley.
    2.54 -\newblock {\em Introduction to Lattices and Order}.
    2.55 -\newblock Cambridge University Press, 1990.
    2.56 +Davey, B.~A., Priestley, H.~A.,
    2.57 +\newblock {\em Introduction to Lattices and Order},
    2.58 +\newblock Cambridge Univ. Press, 1990
    2.59 +
    2.60 +\bibitem{dybjer91}
    2.61 +Dybjer, P.,
    2.62 +\newblock Inductive sets and families in {Martin-L\"of's} type theory and their
    2.63 +  set-theoretic semantics,
    2.64 +\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
    2.65 +  Univ. Press, 1991, pp.~280--306
    2.66 +
    2.67 +\bibitem{IMPS}
    2.68 +Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
    2.69 +\newblock {IMPS}: An interactive mathematical proof system,
    2.70 +\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248
    2.71  
    2.72  \bibitem{hennessy90}
    2.73 -Matthew Hennessy.
    2.74 +Hennessy, M.,
    2.75  \newblock {\em The Semantics of Programming Languages: An Elementary
    2.76 -  Introduction Using Structural Operational Semantics}.
    2.77 -\newblock Wiley, 1990.
    2.78 +  Introduction Using Structural Operational Semantics},
    2.79 +\newblock Wiley, 1990
    2.80 +
    2.81 +\bibitem{huet88}
    2.82 +Huet, G.,
    2.83 +\newblock Induction principles formalized in the {Calculus of Constructions},
    2.84 +\newblock In {\em Programming of Future Generation Computers\/} (1988),
    2.85 +  Elsevier, pp.~205--216
    2.86  
    2.87  \bibitem{melham89}
    2.88 -Thomas~F. Melham.
    2.89 -\newblock Automating recursive type definitions in higher order logic.
    2.90 -\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current
    2.91 -  Trends in Hardware Verification and Automated Theorem Proving}, pages
    2.92 -  341--386. Springer, 1989.
    2.93 +Melham, T.~F.,
    2.94 +\newblock Automating recursive type definitions in higher order logic,
    2.95 +\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
    2.96 +  Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
    2.97 +  pp.~341--386
    2.98 +
    2.99 +\bibitem{milner-ind}
   2.100 +Milner, R.,
   2.101 +\newblock How to derive inductions in {LCF},
   2.102 +\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
   2.103  
   2.104  \bibitem{milner89}
   2.105 -Robin Milner.
   2.106 -\newblock {\em Communication and Concurrency}.
   2.107 -\newblock Prentice-Hall, 1989.
   2.108 +Milner, R.,
   2.109 +\newblock {\em Communication and Concurrency},
   2.110 +\newblock Prentice-Hall, 1989
   2.111 +
   2.112 +\bibitem{monahan84}
   2.113 +Monahan, B.~Q.,
   2.114 +\newblock {\em Data Type Proofs using Edinburgh {LCF}},
   2.115 +\newblock PhD thesis, University of Edinburgh, 1984
   2.116  
   2.117  \bibitem{paulin92}
   2.118 -Christine Paulin-Mohring.
   2.119 -\newblock Inductive definitions in the system {Coq}: Rules and properties.
   2.120 -\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
   2.121 -  December 1992.
   2.122 +Paulin-Mohring, C.,
   2.123 +\newblock Inductive definitions in the system {Coq}: Rules and properties,
   2.124 +\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
   2.125 +  1992
   2.126  
   2.127 -\bibitem{paulson-set-I}
   2.128 -Lawrence~C. Paulson.
   2.129 -\newblock Set theory for verification: {I}. {From} foundations to functions.
   2.130 -\newblock {\em Journal of Automated Reasoning}.
   2.131 -\newblock In press; draft available as Report 271, University of Cambridge
   2.132 -  Computer Laboratory.
   2.133 +\bibitem{paulson87}
   2.134 +Paulson, L.~C.,
   2.135 +\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
   2.136 +\newblock Cambridge Univ. Press, 1987
   2.137  
   2.138  \bibitem{paulson91}
   2.139 -Lawrence~C. Paulson.
   2.140 -\newblock {\em {ML} for the Working Programmer}.
   2.141 -\newblock Cambridge University Press, 1991.
   2.142 +Paulson, L.~C.,
   2.143 +\newblock {\em {ML} for the Working Programmer},
   2.144 +\newblock Cambridge Univ. Press, 1991
   2.145  
   2.146  \bibitem{paulson-coind}
   2.147 -Lawrence~C. Paulson.
   2.148 -\newblock Co-induction and co-recursion in higher-order logic.
   2.149 -\newblock Technical Report 304, University of Cambridge Computer Laboratory,
   2.150 -  July 1993.
   2.151 +Paulson, L.~C.,
   2.152 +\newblock Co-induction and co-recursion in higher-order logic,
   2.153 +\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
   2.154  
   2.155  \bibitem{isabelle-intro}
   2.156 -Lawrence~C. Paulson.
   2.157 -\newblock Introduction to {Isabelle}.
   2.158 -\newblock Technical Report 280, University of Cambridge Computer Laboratory,
   2.159 -  1993.
   2.160 +Paulson, L.~C.,
   2.161 +\newblock Introduction to {Isabelle},
   2.162 +\newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993
   2.163 +
   2.164 +\bibitem{paulson-set-I}
   2.165 +Paulson, L.~C.,
   2.166 +\newblock Set theory for verification: {I}. {From} foundations to functions,
   2.167 +\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
   2.168  
   2.169  \bibitem{paulson-set-II}
   2.170 -Lawrence~C. Paulson.
   2.171 -\newblock Set theory for verification: {II}. {Induction} and recursion.
   2.172 -\newblock Technical Report 312, University of Cambridge Computer Laboratory,
   2.173 -  1993.
   2.174 +Paulson, L.~C.,
   2.175 +\newblock Set theory for verification: {II}. {Induction} and recursion,
   2.176 +\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
   2.177 +
   2.178 +\bibitem{paulson-final}
   2.179 +Paulson, L.~C.,
   2.180 +\newblock A concrete final coalgebra theorem for {ZF} set theory,
   2.181 +\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
   2.182  
   2.183  \bibitem{pitts94}
   2.184 -Andrew~M. Pitts.
   2.185 -\newblock A co-induction principle for recursively defined domains.
   2.186 -\newblock {\em Theoretical Computer Science (Fundamental Studies)}.
   2.187 -\newblock In press; available as Report 252, University of Cambridge Computer
   2.188 -  Laboratory.
   2.189 +Pitts, A.~M.,
   2.190 +\newblock A co-induction principle for recursively defined domains,
   2.191 +\newblock {\em Theoretical Comput. Sci.\/} (1994),
   2.192 +\newblock In press; available as Report 252, Comp. Lab., Univ. Cambridge
   2.193 +
   2.194 +\bibitem{saaltink-fme}
   2.195 +Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
   2.196 +\newblock An {EVES} data abstraction example,
   2.197 +\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
   2.198 +  J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596,
   2.199 +\newblock LNCS 670
   2.200  
   2.201  \bibitem{szasz93}
   2.202 -Nora Szasz.
   2.203 +Szasz, N.,
   2.204  \newblock A machine checked proof that {Ackermann's} function is not primitive
   2.205 -  recursive.
   2.206 -\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
   2.207 -  Environments}, pages 317--338. Cambridge University Press, 1993.
   2.208 +  recursive,
   2.209 +\newblock In {\em Logical Environments}, G.~Huet, G.~Plotkin, Eds. Cambridge
   2.210 +  Univ. Press, 1993, pp.~317--338
   2.211  
   2.212  \end{thebibliography}