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}