Mercurial > cpdt > repo
comparison src/Reflection.v @ 302:7b38729be069
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 * *) |