Mercurial > cpdt > repo

comparison src/Reflection.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents b441010125d4
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
591 (And Truth 591 (And Truth
592 (And Truth 592 (And Truth
593 (And Truth (And Truth (And Truth (And Truth Falsehood)))))) 593 (And Truth (And Truth (And Truth (And Truth Falsehood))))))
594 Falsehood)) 594 Falsehood))
595 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False 595 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False
596 ]] *) 596 ]]
597 *)
597 598
598 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False. 599 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
599 tauto. 600 tauto.
600 Qed. 601 Qed.
601 602
614 and_ind 615 and_ind
615 (fun (_ : True) (H9 : True /\ False) => 616 (fun (_ : True) (H9 : True /\ False) =>
616 and_ind (fun (_ : True) (H11 : False) => False_ind False H11) 617 and_ind (fun (_ : True) (H11 : False) => False_ind False H11)
617 H9) H7) H5) H3) H1) H 618 H9) H7) H5) H3) H1) H
618 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False 619 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False
619 ]] *) 620 ]]
621 *)
620 622
621 623
622 (** * Exercises *) 624 (** * Exercises *)
623 625
624 (** remove printing * *) 626 (** remove printing * *)