more robust pattern: look at longer matches first, added catch-all case;
more private fields;
reworked Recoder: more direct char/string operations, avoids inefficiency of large alternatives (java.util.regex does not optimize regexps);
use "../settings.ML";
use_thy "Even";
use_thy "Mutual";
use_thy "Star";
use_thy "AB";
use_thy "Advanced";