# HG changeset patch
# User HackBot
# Date 1335827712 0
# Node ID 20e728d1d953134223e826c15a88b673d45fef05
# Parent  1e9ba72e22bc4a75a199881ca2d32e2f649d0fbe
<elliott> pastelogs proof general

diff -r 1e9ba72e22bc -r 20e728d1d953 paste/paste.28266
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paste/paste.28266	Mon Apr 30 23:15:12 2012 +0000
@@ -0,0 +1,13 @@
+2007-12-04.txt:16:34:26: <faxathisia> You can use Proof General mode in emacs
+2007-12-04.txt:16:34:45: <faxathisia> anyway Proof General seems good
+2010-07-25.txt:16:02:26: <aliseiphone> Phantom_Hoover: My Coq recommendation: Use Emacs with Proof General. Three window mode and electric mode.
+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.
+2010-12-11.txt:23:26:00: <elliott> Proof General is godly.
+2010-12-11.txt:23:26:21: <elliott> "# See the Proof General Eclipse wiki for screenshots of Proof General in Eclipse."
+2010-12-11.txt:23:40:32: <elliott> Phantom_Hoover: BTW, Proof General can list all the tactics in the system (there's fewer than you think).
+2011-08-05.txt:10:56:07: <elliott> coppro: Umm, Coq is used via Proof General (nicer) or coqtop (interactive command-line system).
+2011-08-05.txt:10:57:37: <elliott> Proof General -- built on top of Emacs -- is by far the nicest way to use Coq.
+2011-08-05.txt:11:00:53: <elliott> Phantom_Hoover: Proof General uses that, right?
+2011-11-16.txt:20:20:31: <Phantom__Hoover> <elliott> http://i.imgur.com/1uOhf.png ;; this is the first time I have ever used three windows in Emacs ← You've never used Proof General?
+2012-04-30.txt:23:12:43: <elliott> Proof General is really, really nice (with a few config tweaks).
+2012-04-30.txt:23:12:56: <elliott> shachaf: Because of Proof General.