doc-src/Ref/ref.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 8979 802acc97fdaf
child 14149 fac076f0c71c
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm@7838
     1
\documentclass[12pt,a4paper]{report}
wenzelm@9695
     2
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../pdfsetup}
wenzelm@2657
     3
lcp@104
     4
%% $Id$
wenzelm@6572
     5
%%\includeonly{}
lcp@104
     6
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
lcp@104
     7
%%% to delete old ones:  \\indexbold{\*[^}]*}
lcp@104
     8
%% run    sedindex ref    to prepare index file
lcp@104
     9
%%% needs chapter on Provers/typedsimp.ML?
wenzelm@6571
    10
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual}
lcp@104
    11
paulson@3128
    12
\author{{\em Lawrence C. Paulson}\\
paulson@3128
    13
        Computer Laboratory \\ University of Cambridge \\
paulson@3128
    14
        \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
paulson@3128
    15
        With Contributions by Tobias Nipkow and Markus Wenzel%
lcp@349
    16
\thanks{Tobias Nipkow, of T. U. Munich, wrote most of
nipkow@3950
    17
  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
nipkow@3950
    18
  and part of
lcp@349
    19
  Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
lcp@349
    20
  Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
paulson@8979
    21
  Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin
paulson@8979
    22
  Simons  and others suggested changes
paulson@3128
    23
  and corrections.  The research has been funded by the EPSRC (grants
paulson@8979
    24
  GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
paulson@8979
    25
  (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
paulson@8979
    26
  Schwerpunktprogramm \emph{Deduktion}.}}  
lcp@349
    27
lcp@104
    28
\makeindex
lcp@104
    29
paulson@3223
    30
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
lcp@104
    31
lcp@104
    32
\pagestyle{headings}
lcp@104
    33
\sloppy
lcp@104
    34
\binperiod     %%%treat . like a binary operator
lcp@104
    35
wenzelm@3108
    36
\railalias{lbrace}{\ttlbrace}
wenzelm@3108
    37
\railalias{rbrace}{\ttrbrace}
berghofe@3098
    38
\railterm{lbrace,rbrace}
berghofe@3098
    39
lcp@104
    40
\begin{document}
wenzelm@3108
    41
\underscoreoff
wenzelm@3108
    42
lcp@104
    43
\index{definitions|see{rewriting, meta-level}}
lcp@104
    44
\index{rewriting!object-level|see{simplification}}
lcp@323
    45
\index{meta-rules|see{meta-rules}}
lcp@286
    46
lcp@286
    47
\maketitle 
lcp@286
    48
\pagenumbering{roman} \tableofcontents \clearfirst
lcp@286
    49
lcp@104
    50
\include{introduction}
lcp@104
    51
\include{goals}
lcp@104
    52
\include{tactic}
lcp@104
    53
\include{tctical}
lcp@104
    54
\include{thm}
lcp@104
    55
\include{theories}
lcp@323
    56
\include{defining}
lcp@323
    57
\include{syntax}
lcp@104
    58
\include{substitution}
lcp@104
    59
\include{simplifier}
lcp@104
    60
\include{classical}
lcp@104
    61
lcp@104
    62
%%seealso's must be last so that they appear last in the index entries
lcp@323
    63
\index{meta-rewriting|seealso{tactics, theorems}}
lcp@104
    64
lcp@286
    65
\begingroup
lcp@286
    66
  \bibliographystyle{plain} \small\raggedright\frenchspacing
paulson@6592
    67
  \bibliography{../manual}
lcp@286
    68
\endgroup
nipkow@302
    69
\include{theory-syntax}
lcp@349
    70
wenzelm@8828
    71
\printindex
lcp@104
    72
\end{document}