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;

added 'value'; tuned;

- put declarations inside a structure (NominalPermeq) - dynamic_thm(s) now looks up theorems in theory associated with proof state (rather than in context associated with simpset) - finite_guess_tac now automatically adds some extra rules about supp to the simpset

- nominal_permeq.ML is now loaded before nominal_package.ML - methods and tactics in nominal_permeq.ML are now defined inside structure NominalPermeq, therefore the names in the method_setup section had to be changed

Implemented proofs of equivariance and finite support for graph of recursion combinator.

Method intro_locales replaced by intro_locales and unfold_locales.

updated

Typo.