> (For now the list of Remaining uses of Proof General / Emacs seems to be > empty. If there is anything remaining, this thread is still open to > submissions.)
Let me make this list nonempty again. In the course of a day, I typically find myself pulling from the Isabelle repository several times. I am encouraged in this by my use of Mercurial queues. So it's not untypical that my HOL image is slightly out of date, usually in a harmless way. Sometimes I fire up Proof General just because I know it will take the image as is instead of forcing me to rebuild it (and waste 4 minutes of my time). This is not a big issue, and I presume that if Proof General stopped to exist, I would adapt my workflow accordingly -- e.g. by getting into the habit of rebuilding HOL after each pull. But the above observation is connected with Andrei's "corridor full of smart people". Sometimes I would just wish Isabelle/jEdit could allow me to do the quick-and-dirty things the more primitive Proof General allowed -- a "I know what I'm doing" flag so to speak. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
