annotate latex/cpdt.tex @ 337:4186722d329b

Hide some more Subset code in template
author Adam Chlipala <adam@chlipala.net>
date Thu, 06 Oct 2011 12:04:55 -0400
parents 4a432659a698
children ad315efc3b6b
rev   line source
adam@311 1 \documentclass[12pt]{report}
adam@311 2 \usepackage[]{inputenc}
adam@311 3 \usepackage[T1]{fontenc}
adam@311 4 \usepackage{fullpage}
adam@311 5 \usepackage{coqdoc}
adam@311 6 \usepackage{amsmath,amssymb}
adam@311 7 \usepackage{url}
adam@311 8 \usepackage{makeidx,hyperref}
adam@311 9
adam@311 10 \title{Certified Programming with Dependent Types}
adam@311 11 \author{Adam Chlipala}
adam@311 12
adam@311 13 \makeindex
adam@311 14
adam@311 15 \begin{document}
adam@311 16
adam@311 17 \maketitle
adam@311 18
adam@311 19 \thispagestyle{empty}
adam@311 20 \mbox{}\vfill
adam@311 21 \begin{center}
adam@311 22
adam@311 23 Copyright Adam Chlipala 2008-2011.
adam@311 24
adam@311 25
adam@311 26 This work is licensed under a
adam@311 27 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adam@311 28 Unported License.
adam@311 29 The license text is available at:
adam@311 30
adam@311 31 \end{center}
adam@311 32
adam@311 33 \begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}
adam@311 34
adam@311 35 \phantomsection
adam@311 36 \tableofcontents
adam@311 37
adam@311 38 \include{Intro.v}
adam@311 39 \include{StackMachine.v}
adam@311 40 \include{InductiveTypes.v}
adam@311 41 \include{Predicates.v}
adam@311 42 \include{Coinductive.v}
adam@311 43 \include{Subset.v}
adam@311 44 \include{MoreDep.v}
adam@311 45 \include{DataStruct.v}
adam@311 46 \include{Equality.v}
adam@311 47 \include{Generic.v}
adam@311 48 \include{Universes.v}
adam@324 49 \include{LogicProg.v}
adam@311 50 \include{Match.v}
adam@311 51 \include{Reflection.v}
adam@311 52 \include{Large.v}
adam@311 53
adam@311 54 \clearpage
adam@311 55 \addcontentsline{toc}{chapter}{Bibliography}
adam@311 56 \bibliographystyle{plain}
adam@311 57 \bibliography{cpdt}
adam@311 58
adam@311 59 \clearpage
adam@311 60 \addcontentsline{toc}{chapter}{Index}
adam@311 61 \printindex
adam@311 62
adam@311 63 \end{document}