rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
rewrite_rule_extra_vars: tuned;
rewritec: omit incr_indexes in most cases, which is a big performance gain;
Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar