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}