revised examples

code streamlining

Ressurect seq attribute accidently removed

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)

Inttab.defined;

some structured proofs on completeness;