annotate paste/paste.16467 @ 6894:1041408d241c
<oerjan> le/rn soviet union/In ancient history, the Soviet Union used to be the THEM. They believed in absurd principles like "Better Red than Dead". Then Ronald Reagan invented Star Wars to destroy it, after which there seemed to be no the THEM for a while.
| author |
HackBot |
| date |
Tue, 16 Feb 2016 21:39:22 +0000 |
| parents |
b30df78e892e |
| children |
|
| rev |
line source |
|
369
|
1 2010-08-21.txt:00:24:22: <botte> coq's syntax is better than agda for people who actually use it. interactive development is possible with Proof General; much nicer than Agda's mode. Proving things in Agda is almost impossible; it is not developed for that at all, while Coq is built around it. ProofGeneral makes it even nicer.
|
|
|
2 2010-08-21.txt:17:24:29: <alise> use proofgeneral with electric mode and three window mode
|
|
|
3 2010-08-21.txt:17:25:05: <alise> with proofgeneral electric three-window you have one window for your file
|
|
|
4 2010-08-21.txt:17:26:54: <Phantom_Hoover> alise, I haven't tried Proofgeneral yet, though.
|
|
|
5 2010-08-22.txt:21:59:25: <Vonlebio> OK, why has Proofgeneral's indentation behaviour changed all of a sudden?
|
|
|
6 2010-11-28.txt:17:45:30: * Phantom_Hoover decides to reduce his confusion with ProofGeneral steppery.
|
|
|
7 2011-04-07.txt:20:07:30: <elliott> proofgeneral's interface to the toplevel.
|
|
|
8 2011-04-07.txt:20:08:19: <elliott> augur: turn on three window mode and electric terminator in proofgeneral
|
