# HG changeset patch # User lcp # Date 764424312 -3600 # Node ID 63a0077dd9f27b76a1ea7eacbb6acf5b6c544495 # Parent cc69ef31cfc36bb38d506bb8102b92f47602d4d7 first draft of Springer volume diff -r cc69ef31cfc3 -r 63a0077dd9f2 doc-src/iman.sty --- a/doc-src/iman.sty Wed Mar 23 11:32:21 1994 +0100 +++ b/doc-src/iman.sty Wed Mar 23 13:05:12 1994 +0100 @@ -1,14 +1,16 @@ -\typeout{Isabelle Manual Page Layout} - -% iman.sty +% iman.sty : Isabelle Manual Page Layout % -\typeout{Document Style iman. Released 15 September 1992} +\typeout{Document Style iman. Released 17 February 1994} -\hyphenation{Isa-belle} +\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly} +\hyphenation{data-type data-types co-data-type co-data-types } + +\let\ts=\thinspace %%%INDEXING use sedindex to process the index %index, putting page numbers of definitions in boldface \newcommand\bold[1]{{\bf#1}} +\newcommand\fnote[1]{#1n} \newcommand\indexbold[1]{\index{#1|bold}} %for cross-references: 2nd argument (page number) is ignored @@ -23,12 +25,6 @@ \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@} -%%Euro-style date: 20 September 1955 -\def\today{\number\day\space\ifcase\month\or -January\or February\or March\or April\or May\or June\or -July\or August\or September\or October\or November\or December\fi -\space\number\year} - %%% underscores as ordinary characters, not for subscripting %% use @ or \sb for subscripting; use \at for @ %% only works in \tt font @@ -57,10 +53,10 @@ %%%% ``WARNING'' environment \def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}} \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 - \baselineskip=0.9\baselineskip - \noindent \hangindent\parindent \hangafter=-2 - \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% - {\par\endgroup\medbreak} + \small %%WAS\baselineskip=0.9\baselineskip + \noindent \hangindent\parindent \hangafter=-2 + \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% + {\par\endgroup\medbreak} %%%% Standard logical symbols @@ -69,13 +65,10 @@ \let\disj=\vee \let\imp=\rightarrow \let\bimp=\leftrightarrow -\newcommand\all[1]{\forall#1.} %quantification +\newcommand\all[1]{\forall#1.} %quantification \newcommand\ex[1]{\exists#1.} \newcommand{\pair}[1]{\langle#1\rangle} -\newenvironment{example}{\begin{Example}\rm}{\end{Example}} -\newtheorem{Example}{Example}[chapter] - \newcommand\lbrakk{\mathopen{[\![}} \newcommand\rbrakk{\mathclose{]\!]}} \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj @@ -86,9 +79,6 @@ \let\inter=\bigcap \let\union=\bigcup -\newcommand{\rew}{\mathop{\longrightarrow}} -\newcommand{\rewer}{\mathop{\longleftrightarrow}} - \def\ML{{\sc ml}} \def\OBJ{{\sc obj}} @@ -110,40 +100,16 @@ \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt} \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt} -\chardef\ttilde=`\~ % A tilde for \tt font -\chardef\ttback=`\\ % A backslash for \tt font -\chardef\ttlbrace=`\{ % A left brace for \tt font -\chardef\ttrbrace=`\} % A right brace for \tt font +\chardef\ttilde=`\~ % A tilde for \tt font +\chardef\ttback=`\\ % A backslash for \tt font +\chardef\ttlbrace=`\{ % A left brace for \tt font +\chardef\ttrbrace=`\} % A right brace for \tt font \newfont{\sltt}{cmsltt10} %% for output from terminal sessions \newcommand\out{\ \sltt} -%Indented, boxed alltt environment; uses \small\tt font -%\leftmargini is LaTeX's first-level indentation for items (2.5em) -%@endparenv is LaTeX's trick for preventing indentation of next paragraph -\newenvironment{ttbox}{\par\nobreak\vskip-2pt - \vbox\bgroup \small\begin{alltt} \leftskip\leftmargini}% - {\end{alltt}\egroup\vskip-7pt\@endparenv} -\newcommand\ttbreak{\end{ttbox}\vskip-10pt\begin{ttbox}} - - -%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage -\newcommand\clearfirst{\clearpage\ifodd\c@page\else - \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi - \pagenumbering{arabic}} - -%%%Ruled chapter headings -\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf - #1 \vskip 14pt\hrule height1pt} -\def\@makechapterhead#1{ { \parindent 0pt - \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par - \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } } - -\def\@makeschapterhead#1{ { \parindent 0pt \raggedright - \@rulehead{#1} \par \nobreak \vskip 40pt } } - % "itmath.sty" use cmr italic for letters in math mode and get the -% usual letter spacing of text mode. +% usual letter spacing of text mode. % % Michael Lawley, April 1993 % (lawley@cit.gu.edu.au) @@ -178,4 +144,4 @@ \@setmcodes{`a}{`z}{"7\@tempa 61} \ifx\define@mathgroup\undefined\else - \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi + \define@mathgroup\mv@normal{\itfam}{cmr}{m}{it}\fi diff -r cc69ef31cfc3 -r 63a0077dd9f2 doc-src/ind-defs.bbl --- a/doc-src/ind-defs.bbl Wed Mar 23 11:32:21 1994 +0100 +++ b/doc-src/ind-defs.bbl Wed Mar 23 13:05:12 1994 +0100 @@ -1,105 +1,143 @@ \begin{thebibliography}{10} \bibitem{abramsky90} -Samson Abramsky. -\newblock The lazy lambda calculus. -\newblock In David~A. Turner, editor, {\em Resesarch Topics in Functional - Programming}, pages 65--116. Addison-Wesley, 1977. +Abramsky, S., +\newblock The lazy lambda calculus, +\newblock In {\em Resesarch Topics in Functional Programming}, D.~A. Turner, + Ed. Addison-Wesley, 1977, pp.~65--116 \bibitem{aczel77} -Peter Aczel. -\newblock An introduction to inductive definitions. -\newblock In J.~Barwise, editor, {\em Handbook of Mathematical Logic}, pages - 739--782. North-Holland, 1977. +Aczel, P., +\newblock An introduction to inductive definitions, +\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed. + North-Holland, 1977, pp.~739--782 \bibitem{aczel88} -Peter Aczel. -\newblock {\em Non-Well-Founded Sets}. -\newblock CSLI, 1988. +Aczel, P., +\newblock {\em Non-Well-Founded Sets}, +\newblock CSLI, 1988 \bibitem{bm79} -Robert~S. Boyer and J~Strother Moore. -\newblock {\em A Computational Logic}. -\newblock Academic Press, 1979. +Boyer, R.~S., Moore, J.~S., +\newblock {\em A Computational Logic}, +\newblock Academic Press, 1979 \bibitem{camilleri92} -J.~Camilleri and T.~F. Melham. +Camilleri, J., Melham, T.~F., \newblock Reasoning with inductively defined relations in the {HOL} theorem - prover. -\newblock Technical Report 265, University of Cambridge Computer Laboratory, - August 1992. + prover, +\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, August 1992 \bibitem{davey&priestley} -B.~A. Davey and H.~A. Priestley. -\newblock {\em Introduction to Lattices and Order}. -\newblock Cambridge University Press, 1990. +Davey, B.~A., Priestley, H.~A., +\newblock {\em Introduction to Lattices and Order}, +\newblock Cambridge Univ. Press, 1990 + +\bibitem{dybjer91} +Dybjer, P., +\newblock Inductive sets and families in {Martin-L\"of's} type theory and their + set-theoretic semantics, +\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge + Univ. Press, 1991, pp.~280--306 + +\bibitem{IMPS} +Farmer, W.~M., Guttman, J.~D., Thayer, F.~J., +\newblock {IMPS}: An interactive mathematical proof system, +\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248 \bibitem{hennessy90} -Matthew Hennessy. +Hennessy, M., \newblock {\em The Semantics of Programming Languages: An Elementary - Introduction Using Structural Operational Semantics}. -\newblock Wiley, 1990. + Introduction Using Structural Operational Semantics}, +\newblock Wiley, 1990 + +\bibitem{huet88} +Huet, G., +\newblock Induction principles formalized in the {Calculus of Constructions}, +\newblock In {\em Programming of Future Generation Computers\/} (1988), + Elsevier, pp.~205--216 \bibitem{melham89} -Thomas~F. Melham. -\newblock Automating recursive type definitions in higher order logic. -\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current - Trends in Hardware Verification and Automated Theorem Proving}, pages - 341--386. Springer, 1989. +Melham, T.~F., +\newblock Automating recursive type definitions in higher order logic, +\newblock In {\em Current Trends in Hardware Verification and Automated Theorem + Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989, + pp.~341--386 + +\bibitem{milner-ind} +Milner, R., +\newblock How to derive inductions in {LCF}, +\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980 \bibitem{milner89} -Robin Milner. -\newblock {\em Communication and Concurrency}. -\newblock Prentice-Hall, 1989. +Milner, R., +\newblock {\em Communication and Concurrency}, +\newblock Prentice-Hall, 1989 + +\bibitem{monahan84} +Monahan, B.~Q., +\newblock {\em Data Type Proofs using Edinburgh {LCF}}, +\newblock PhD thesis, University of Edinburgh, 1984 \bibitem{paulin92} -Christine Paulin-Mohring. -\newblock Inductive definitions in the system {Coq}: Rules and properties. -\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, - December 1992. +Paulin-Mohring, C., +\newblock Inductive definitions in the system {Coq}: Rules and properties, +\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec. + 1992 -\bibitem{paulson-set-I} -Lawrence~C. Paulson. -\newblock Set theory for verification: {I}. {From} foundations to functions. -\newblock {\em Journal of Automated Reasoning}. -\newblock In press; draft available as Report 271, University of Cambridge - Computer Laboratory. +\bibitem{paulson87} +Paulson, L.~C., +\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}, +\newblock Cambridge Univ. Press, 1987 \bibitem{paulson91} -Lawrence~C. Paulson. -\newblock {\em {ML} for the Working Programmer}. -\newblock Cambridge University Press, 1991. +Paulson, L.~C., +\newblock {\em {ML} for the Working Programmer}, +\newblock Cambridge Univ. Press, 1991 \bibitem{paulson-coind} -Lawrence~C. Paulson. -\newblock Co-induction and co-recursion in higher-order logic. -\newblock Technical Report 304, University of Cambridge Computer Laboratory, - July 1993. +Paulson, L.~C., +\newblock Co-induction and co-recursion in higher-order logic, +\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993 \bibitem{isabelle-intro} -Lawrence~C. Paulson. -\newblock Introduction to {Isabelle}. -\newblock Technical Report 280, University of Cambridge Computer Laboratory, - 1993. +Paulson, L.~C., +\newblock Introduction to {Isabelle}, +\newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993 + +\bibitem{paulson-set-I} +Paulson, L.~C., +\newblock Set theory for verification: {I}. {From} foundations to functions, +\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389 \bibitem{paulson-set-II} -Lawrence~C. Paulson. -\newblock Set theory for verification: {II}. {Induction} and recursion. -\newblock Technical Report 312, University of Cambridge Computer Laboratory, - 1993. +Paulson, L.~C., +\newblock Set theory for verification: {II}. {Induction} and recursion, +\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993 + +\bibitem{paulson-final} +Paulson, L.~C., +\newblock A concrete final coalgebra theorem for {ZF} set theory, +\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994 \bibitem{pitts94} -Andrew~M. Pitts. -\newblock A co-induction principle for recursively defined domains. -\newblock {\em Theoretical Computer Science (Fundamental Studies)}. -\newblock In press; available as Report 252, University of Cambridge Computer - Laboratory. +Pitts, A.~M., +\newblock A co-induction principle for recursively defined domains, +\newblock {\em Theoretical Comput. Sci.\/} (1994), +\newblock In press; available as Report 252, Comp. Lab., Univ. Cambridge + +\bibitem{saaltink-fme} +Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I., +\newblock An {EVES} data abstraction example, +\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993), + J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596, +\newblock LNCS 670 \bibitem{szasz93} -Nora Szasz. +Szasz, N., \newblock A machine checked proof that {Ackermann's} function is not primitive - recursive. -\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical - Environments}, pages 317--338. Cambridge University Press, 1993. + recursive, +\newblock In {\em Logical Environments}, G.~Huet, G.~Plotkin, Eds. Cambridge + Univ. Press, 1993, pp.~317--338 \end{thebibliography}