Tue, 10 Nov 2015 19:50:56 +0100 ignore pointless/unused options;
wenzelm [Tue, 10 Nov 2015 19:50:56 +0100] rev 61615
ignore pointless/unused options;
Tue, 10 Nov 2015 19:03:29 +0100 added document antiquotation @{theory_text};
wenzelm [Tue, 10 Nov 2015 19:03:29 +0100] rev 61614
added document antiquotation @{theory_text}; tuned document;
Tue, 10 Nov 2015 16:03:59 +0100 allow open symboloid;
wenzelm [Tue, 10 Nov 2015 16:03:59 +0100] rev 61613
allow open symboloid;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip