Mercurial > cpdt > repo
annotate latex/cpdt.tex @ 473:39c204d2262c
Remove hyperlinks to standard library, which were broken anyway
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 22 Oct 2012 13:28:54 -0400 |
| parents | 62475ab7570b |
| children | 40a9a36844d6 |
| rev | line source |
|---|---|
| adam@311 | 1 \documentclass[12pt]{report} |
| adam@311 | 2 \usepackage[]{inputenc} |
| adam@311 | 3 \usepackage[T1]{fontenc} |
| adam@468 | 4 \usepackage{lmodern} |
| adam@311 | 5 \usepackage{fullpage} |
| adam@311 | 6 \usepackage{coqdoc} |
| adam@311 | 7 \usepackage{amsmath,amssymb} |
| adam@311 | 8 \usepackage{url} |
| adam@311 | 9 \usepackage{makeidx,hyperref} |
| adam@311 | 10 |
| adam@311 | 11 \title{Certified Programming with Dependent Types} |
| adam@311 | 12 \author{Adam Chlipala} |
| adam@311 | 13 |
| adam@311 | 14 \makeindex |
| adam@311 | 15 |
| adam@311 | 16 \begin{document} |
| adam@311 | 17 |
| adam@311 | 18 \maketitle |
| adam@311 | 19 |
| adam@311 | 20 \thispagestyle{empty} |
| adam@311 | 21 \mbox{}\vfill |
| adam@311 | 22 \begin{center} |
| adam@311 | 23 |
| adam@370 | 24 Copyright Adam Chlipala 2008-2012. |
| adam@311 | 25 |
| adam@311 | 26 |
| adam@311 | 27 This work is licensed under a |
| adam@311 | 28 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
| adam@311 | 29 Unported License. |
| adam@311 | 30 The license text is available at: |
| adam@311 | 31 |
| adam@311 | 32 \end{center} |
| adam@311 | 33 |
| adam@311 | 34 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center} |
| adam@311 | 35 |
| adam@311 | 36 \phantomsection |
| adam@311 | 37 \tableofcontents |
| adam@311 | 38 |
| adam@311 | 39 \include{Intro.v} |
| adam@311 | 40 \include{StackMachine.v} |
| adam@311 | 41 \include{InductiveTypes.v} |
| adam@311 | 42 \include{Predicates.v} |
| adam@311 | 43 \include{Coinductive.v} |
| adam@353 | 44 \include{Subset.v} |
| adam@350 | 45 \include{GeneralRec.v} |
| adam@311 | 46 \include{MoreDep.v} |
| adam@311 | 47 \include{DataStruct.v} |
| adam@311 | 48 \include{Equality.v} |
| adam@311 | 49 \include{Generic.v} |
| adam@311 | 50 \include{Universes.v} |
| adam@324 | 51 \include{LogicProg.v} |
| adam@311 | 52 \include{Match.v} |
| adam@311 | 53 \include{Reflection.v} |
| adam@311 | 54 \include{Large.v} |
| adam@381 | 55 \include{ProgLang.v} |
| adam@383 | 56 \include{Conclusion.v} |
| adam@311 | 57 |
| adam@311 | 58 \clearpage |
| adam@311 | 59 \addcontentsline{toc}{chapter}{Bibliography} |
| adam@311 | 60 \bibliographystyle{plain} |
| adam@311 | 61 \bibliography{cpdt} |
| adam@311 | 62 |
| adam@311 | 63 \clearpage |
| adam@311 | 64 \addcontentsline{toc}{chapter}{Index} |
| adam@311 | 65 \printindex |
| adam@311 | 66 |
| adam@311 | 67 \end{document} |