Sort search results in order of relevance, where relevance =
a) better if 0 premises for intro or 1 premise for elim/dest rules
b) better if substitution size wrt to current goal is smaller
Only applies to intro, dest, elim, and simp
(contributed by Rafal Kolanski, NICTA)
Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef Locales LaTeXsugar