Sat, 16 Nov 2013 17:52:01 +0100 wenzelm tuned signature -- clarified Proof General legacy;
Sat, 16 Nov 2013 17:39:11 +0100 wenzelm toplevel function "use" refers to raw ML bootstrap environment;
Sat, 16 Nov 2013 17:04:17 +0100 wenzelm obsolete;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip