Introduction of "whitelist": theorems forced past the relevance filter

Slight simplification of proofs

Removal of obsolete strategies. Initial support for locales: Frees and Consts treated similarly.

comment for conjI added

translations -> abbreviations (a cool feature)

fixed example;

mark_boundT: produce well-typed term;

subtract (op =); pretty_proof: no abbrevs;

avoid polymorphic equality; tuned;

avoid polymorphic equality; subtract (op =);

moved gen_eq_set to library.ML;

added ~$$ (negative literal); combinators: avoid code duplication; tuned extend_lexicon;

avoid polymorphic equality;

remove (op =); tuned;

gen_eq_set, remove (op =);

abbreviation upto, length;

added subtract; tuned;

subtract (op =);

remove (op =);

Now SML/NJ-friendly (IntInf)

Removal of unnecessary simprules: simproc cancel_numerals now works without add_Suc, while the reason for the horrible isolateSuc is not known.

interpret: Proof.assert_forward_or_chain;

subsetI is often necessary

Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer need to be outermost.

Tuned signature of Locale.add_locale(_i).

simplified mg_domain (use Sign.classes/arities_of); removed unused lift_local_theory_yield;

made $$ and "this" monomorphic (string);

tuned;

export arities_of instead of classes_arities_of;

updated;

renamed const less to lt;

renamed constant less in lattice