removed the "tagging" feature

made the conversion of elimination rules more robust

Literals aren't sorted any more.

Literals aren't sorted any more. Output overloaded constants' type var instantiations.

fixed let-simproc ----------------------------------------------------------------------

Isar: 'print_facts' prints all local facts;

print_lthms: include unnamed facts from index; tuned;

added content;

added props selector;

print_facts: all facts;

add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;

instantiate_tfrees: Thm.generalize;

removed parrot comment;

Proof by guessing.

guess: proper context for polymorphic parameters; tuned;

polymorphic: always generalize wrt. used_types;

varifyT: no longer pervasive;

added generalize/instantiate_option;

added map_proof_terms_option; tuned generalize, instantiate;

added generalize; removed obsolete assume_ax, tvars_intr_list;

Thm.varifyT;

added ex/Guess.thy;

skip_proofs: do not skip proofs of schematic goals (warning);

added schematic_goal;

added 'unfolding';

added simplification rules to the fresh_guess tactic

made calc_atm stronger by including some relative obvious simplification rules

Locales no longer generate views. The following functions have changed signatures: Locale.init, Locale.add_thmss, Locale.read/cert_context_statement.

added 'definition', 'unfolding', 'done'; tuned;

tuned;