wneuper/isa: doc-src/Ref/ref.tex@e9d5bcae8351

     1 \documentclass[12pt]{report}

     2 \usepackage{a4}

     4 \makeatletter

     5 \input{../proof.sty}

     6 \input{../rail.sty}

     7 \input{../iman.sty}

     8 \input{../extra.sty}

     9 \makeatother

    11 %% $Id$

    12 %%\includeonly{}

    13 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}

    14 %%% to delete old ones:  \\indexbold{\*[^}]*}

    15 %% run    sedindex ref    to prepare index file

    16 %%% needs chapter on Provers/typedsimp.ML?

    17 \title{The Isabelle Reference Manual}

    19 \author{{\em Lawrence C. Paulson}\\

    20         Computer Laboratory \\ University of Cambridge \\

    21         \texttt{lcp@cl.cam.ac.uk}\\[3ex]

    22         With Contributions by Tobias Nipkow and Markus Wenzel%

    23 \thanks{Tobias Nipkow, of T. U. Munich, wrote most of

    24   Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},

    25   and part of

    26   Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to

    27   Chapter~\protect\ref{theories}.  Markus Wenzel contributed to

    28   Chapter~\protect\ref{chap:syntax}.  Sara Kalvala, Martin Simons and others

    29   suggested changes

    30   and corrections.  The research has been funded by the EPSRC (grants

    31   GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453:

    32   Types.}}

    34 \makeindex

    36 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

    38 \pagestyle{headings}

    39 \sloppy

    40 \binperiod     %%%treat . like a binary operator

    42 \railalias{lbrace}{\ttlbrace}

    43 \railalias{rbrace}{\ttrbrace}

    44 \railterm{lbrace,rbrace}

    46 \begin{document}

    47 \underscoreoff

    49 \index{definitions|see{rewriting, meta-level}}

    50 \index{rewriting!object-level|see{simplification}}

    51 \index{meta-rules|see{meta-rules}}

    53 \maketitle

    54 \pagenumbering{roman} \tableofcontents \clearfirst

    56 \include{introduction}

    57 \include{goals}

    58 \include{tactic}

    59 \include{tctical}

    60 \include{thm}

    61 \include{theories}

    62 \include{defining}

    63 \include{syntax}

    64 \include{substitution}

    65 \include{simplifier}

    66 \include{classical}

    68 %%seealso's must be last so that they appear last in the index entries

    69 \index{meta-rewriting|seealso{tactics, theorems}}

    71 \begingroup

    72   \bibliographystyle{plain} \small\raggedright\frenchspacing

    73   \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}

    74 \endgroup

    75 \include{theory-syntax}

    77 \input{ref.ind}

    78 \end{document}

author	nipkow
	Mon, 20 Oct 1997 11:53:42 +0200
changeset 3950	e9d5bcae8351
parent 3285	9a3fe25f30bb
child 4383	25704541008b
permissions	-rw-r--r--