etc/settings

--- a/etc/settings	Wed Sep 14 14:17:32 2016 +0200
+++ b/etc/settings	Wed Sep 14 14:37:38 2016 +0200
@@ -121,11 +121,10 @@
 
 
 ###
-### Symbol rendering and abbreviations
+### Symbol rendering
 ###
 
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
-ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs"
 
 
 ###