added force_proofs (based on thms ever passed through enter_thms);

tuned;

eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion; eliminated obsolete alias rewtac for rewrite_goals_tac;

moved table of standard Isabelle symbols to isar-ref manual;

added isabelle-implementation manual;

disabled threads -- as advertized;

changes by Fabian Immler: improved handling of prover errors; explicit treatment of clauses that are too trivial for resolution;

Code for switching to new locales.

add_thmss

Activate elements moved to element.ML.

finish: force proofs;

finish_proof: undefined promises may occur here;

tuned promise/fullfill;

unified treatment of PAxm/Oracle/Promise in basic proof term operations; refined promise/fulfill: maintain proper type instantiation, disallow term variables; thm_proof: uniform finish_proof before and after fulfill;

removed Induct/Mutil.thy -- the file has been moved to AFP;

simplified thm_deps -- no need to build a graph datastructure;

removed Induct/Mutil.thy -- the file has been moved to AFP;

-> AFP

tuned unfold_locales invocation

explicit name morphism function for locale interpretation

Name.name_with_prefix (temporarily)

adjusted locale signature to *_cmd convention

whitespace tuning

Generic activation of locales.

proof_body/pthm: removed redundant types field;

put_name/thm_proof: promises are filled with fulfilled proofs; tuned;

proof_body/pthm: removed redundant types field; fold_proof_atoms: unified recursive case with fold_body_thms; tuned signature;

clarified Thm.proof_body_of vs. Thm.proof_of;

- Corrected order of quantification over Frees. - Fixed bug in handling of TFrees that caused variable order to get mixed up.

Frees in PThms are now quantified in the order of their appearance in the proposition as well, to make it compatible (again) with variable order used by forall_intr_frees.