Mercurial > cpdt > repo

diff src/Predicates.v @ 439:393b8ed99c2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of improvements to vertical spacing, up through end of InductiveTypes
author Adam Chlipala <adam@chlipala.net>
date Mon, 30 Jul 2012 13:21:36 -0400
parents 5f25705a10ea
children f923024bd284
line wrap: on
line diff
--- a/src/Predicates.v	Fri Jul 27 16:55:30 2012 -0400
+++ b/src/Predicates.v	Mon Jul 30 13:21:36 2012 -0400
@@ -174,16 +174,15 @@
     Every proof of a conjunction provides proofs for both conjuncts, so we get a single subgoal reflecting that.  We can proceed by splitting this subgoal into a case for each conjunct of [Q /\ P].%\index{tactics!split}% *)
 
     split.
-(** %\vspace{.1in} \noindent 2 \coqdockw{subgoals}\vspace{-.1in}%#<tt>2 subgoals</tt>#
-[[
+(** 2 subgoals
   
   H : P
   H0 : Q
   ============================
    Q
-]]
-%\noindent \coqdockw{subgoal} 2 \coqdockw{is}:%#<tt>subgoal 2 is</tt>#
-[[
+
+subgoal 2 is
+
    P
  
  ]]
@@ -212,15 +211,15 @@
     (** As in the proof for [and], we begin with case analysis, though this time we are met by two cases instead of one. *)
 
     destruct 1.
-(** %\vspace{.1in} \noindent 2 \coqdockw{subgoals}\vspace{-.1in}%#<tt>2 subgoals</tt>#
-[[
+(** [[
+2 subgoals
   
   H : P
   ============================
    Q \/ P
-]]
-%\noindent \coqdockw{subgoal} 2 \coqdockw{is}:%#<tt>subgoal 2 is</tt>#
-[[
+
+subgoal 2 is
+
  Q \/ P
  
  ]]