# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1343850770 14400
# Node ID cbfd23b4364de7ba3205a08adee5fbfe8fbca284
# Parent  f923024bd28419c931956bdf7f190e35273a0936
Vertical spacing pass through GeneralRec

diff -r f923024bd284 -r cbfd23b4364d src/GeneralRec.v
--- a/src/GeneralRec.v	Mon Jul 30 16:50:02 2012 -0400
+++ b/src/GeneralRec.v	Wed Aug 01 15:52:50 2012 -0400
@@ -220,7 +220,7 @@
 Eval compute in mergeSort leb (1 :: 2 :: 36 :: 8 :: 19 :: nil).
 (** [= 1 :: 2 :: 8 :: 19 :: 36 :: nil] *)
 
-(** Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *)
+(** %\smallskip{}%Since the subject of this chapter is merely how to define functions with unusual recursion structure, we will not prove any further correctness theorems about [mergeSort]. Instead, we stop at proving that [mergeSort] has the expected computational behavior, for all inputs, not merely the one we just tested. *)
 
 (* begin thide *)
 Theorem mergeSort_eq : forall A (le : A -> A -> bool) ls,