*** empty log message ***

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;

clean: added HOL-Main;

rewrite_proof: simplified simprocs (no name required);

multithreading support for polyml-5.2 actually disabled -- as advertized;

Initial part of locale reimplementation.

Made local_note_prefix public.

re-educated guess

namify and name_decl combinators

Name.is_nothing

lemmas about dom and minus / insert

added length_unique operation for code generation

updated generated files;

removed "includes" element (lost update?);

updated generated files;

added section "Explicit instantiation within a subgoal context";

renamed "Rules" to "Object-level rules";

more on basic tactics;

basic ML reference for tactics;

added section "Tactics";

more contributors;

separate section "Inspecting the syntax" for print_syntax;

misc tuning of inner syntax;

added inner lexical syntax, reusing outer one;

misc tuning;

tuned outer lexical syntax; fixed var/tvar: really need question marks here;

more tuning of Pure grammer;

updated and elaborated Pure grammer;

added Pure grammer (from old ref manual);

mixfix annotations: verbatim for special symbols;

added section "The Pure grammar" (incomplete version, based on old ref manual);

added section "Priority grammars" (variant from old ref manual);

added section "Co-regularity of type classes and arities" (variant from old ref manual); tuned arity spacing;

minor tuning (according to old ref manual);

misc tuning and rearrangement of section "Printing logical entities";

misc tuning and rearrangement of section "Printing logical entities";

fixed/tuned syntax for attribute "tagged";

added pretty printing options (from old ref manual);

separate chapter "Inner syntax --- the term language";

updated/refined types of Isar language elements, removed special LaTeX macros;

unified use of declaration environment with IsarImplementation; tuned ML decls;

ignore ThyOutput.source flag;

added bind_thm, bind_thms;

tuned section "Incorporating ML code"; moved method_setup to separate section "Defining proof methods";

tuned section "Oracles";

tuned section arrangement;

moved section "Proof method expressions" to proof chapter; minor rearrangement of proof sections;

more on mixfix annotations (updated material from old ref manual);

tuned;

moved section "Document preparation" to front;

updated section "Markup via command tags";

renamed "formal comments" to "document comments"; tuned section "Markup commands"; updated/tuned section "Document Antiquotations";

renamed "formal comments" to "document comments";

tuned "Markup commands";

tuned intro of "Document preparation";

reworked "Defining Theories";

removed Assert.thy

dropped superfluos eval_conv

moved assert to Heap_Monad.thy

simproc for let

improved handling of !!/==> for eval and normalization

proper name morphisms for locales

consider prefixes for name bindings of simprocs (a first approximation)

diagnostic output for name bindings

Some modifications in code for proving arities to make it work for datatype definitions with additional sort constraints.