fixed

Added new fold operator and renamed the old oe to fold_image.

Type inference for elements through syntax module.

Use 'if' in connection with 'is_some' and 'the'.

Basic types not qualified.

Enable switching to new locales during session.

explicit inhabitance proof

fulfill_proof/thm_proof: commuted lazyness; join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);

fulfill_proof/thm_proof: commuted lazyness;

removed lemmas called lemma1 and lemma2

force_proofs after cumulative use_thys; PureThy.force_proofs;

signed_string_of_int for priorities; tuned;

added force_proofs; join_futures: no errors here;

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.

adapted PThm and MinProof;

retrieve thm deps from proof_body; removed obsolete enable/disable operation;

retrieve thm deps from proof_body;

adapted PThm;

proof_of_term: removed obsolete disambiguisation table; adapted PThm; Thm.proof_of returns proof_body;

rewrite_proof: simplified simprocs (no name required); adapted PThm; fold_proof_atoms;

Thm.proof_of returns proof_body; adapted PThm;

refined notion of derivation, consiting of promises and proof_body; removed oracle_of (would require detailed check wrt. promises); proof_of returns proof_body;

reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial); added type proof_body, which covers oracles and thms of local proof; added general fold_body_thms, fold_proof_atoms; removed thms_of_proof, thms_of_proof', axms_of_proof; slightly more abstract handling of body content (oracles, thms); rewrite_proof: simplified simprocs (no name required); thm_proof: lazy fulfillment of promises;

pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);

ProofSyntax.proof_of_term: removed obsolete disambiguisation table; adapted PThm;

name_of_thm: Proofterm.fold_proof_atoms; Thm.proof_of returns proof_body;

Thm.proof_of returns proof_body;