Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.

Replaced iteration combinator by recursion combinator.

detection of definitions of relevant constants

Only display atpset theorems if Output.show_debug_msgs is true.

added the first two simple proofs of the recursion combinator

comment fixed

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.