simplified the proof at_fin_set_supp

changed abbreviation for "infinite" back to translation because something didn't work during (output).

lazy patterns in lambda abstractions

changed the it_prm proof to work for recursion

tuned some proofs

Removed occurrences of makestring, which does not exist in SML/NJ.

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;