Mercurial > cpdt > repo
changeset 43:9bdbc43d510e
Make Chap. 3 title less grand
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 15 Sep 2008 10:05:37 -0400 |
parents | 7021e94dbbec |
children | b1e137b4aafe |
files | src/InductiveTypes.v src/Intro.v |
diffstat | 2 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/InductiveTypes.v Sat Sep 13 14:35:14 2008 -0400 +++ b/src/InductiveTypes.v Mon Sep 15 10:05:37 2008 -0400 @@ -16,7 +16,7 @@ (* end hide *) -(** %\chapter{Inductive Types}% *) +(** %\chapter{Introducing Inductive Types}% *) (** In a sense, CIC is built from just two relatively straightforward features: function types and inductive types. From this modest foundation, we can prove effectively all of the theorems of math and carry out effectively all program verifications, with enough effort expended. This chapter introduces induction and recursion in Coq and shares some "design patterns" for overcoming common pitfalls with them. *)
--- a/src/Intro.v Sat Sep 13 14:35:14 2008 -0400 +++ b/src/Intro.v Mon Sep 15 10:05:37 2008 -0400 @@ -185,7 +185,7 @@ \hline Some Quick Examples & \texttt{StackMachine.v} \\ \hline -Inductive Types & \texttt{InductiveTypes.v} \\ +Introducing Inductive Types & \texttt{InductiveTypes.v} \\ \hline \end{tabular} \end{center}