Merged again.

Merged.

News entry: inheritance of mixins; print_interps.

Avoid administrative overhead for identity mixins.

tuned;

moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;

added Ctermtab, cterm_cache, thm_cache; tuned;

added term_cache; tuned;

Concurrently cached values.

tuned header; tuned whitespace;

core_sos_tac: SUBPROOF body operates on subgoal 1; tuned;

merged

updated generated files;

enable slow-motion mode to accomodate unsynchronized refs within theory sources;

avoid unsynchronized refs within theory sources;

explicitly Unsynchronized;

additional fixes in normarith.ML due to FuncFun and FuncUtil changes

changed core_sos_tac to use SUBPROOF

replaced and tuned uses of foldr1

tuned FuncFun and FuncUtil structure in positivstellensatz.ML

removed opening of structures

merged

merged

merged

made spass additional default prover

merged

Proved a new theorem: nat_to_nat2_inj

turned unsynchronized ref into synchronized var

merged

resolved conflict

record max lemmas used

Lazy evaluation with memoing (sequential version).

more official status of sequential implementations; tuned;

separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations;

added Task_Queue.depend (again) -- light-weight version for transitive graph; Future.join_results: record explicit dependency, detect direct task-task join cycles; Future.join_results: no change of interruptibility, allows to interrupt wait; added Future.worker_task; ThyInfo.schedule_futures: uninterruptible outer join;

handle Pattern.MATCH, not arbitrary exceptions; misc tuning, trying to reduce line length a bit;

more precise dependencies;

eliminated redundant parameters;

back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;

avoid mixed l/r infixes, which do not work in some versions of SML;

tuned;

merged

explicitly Unsynchronized

Merged.

Propagation of mixins for interpretation; reactivated diagnostic command print_interps.

Archive registrations by external view.

Stricter test: raise error if registration generates duplicate theorem.

Explicit management of registration mixins.

Improved comments and api names.

eliminated dead code, redundant bindings and parameters; use === term operator, which is defined here; handle Type.TYPE_MATCH, not arbitrary exceptions; misc tuning and simplification;

misc tuning and simplification; be explicit about expressions involving infixes with non-obvious priorities; removed dead code; some attempts to recover basic Isabelle coding conventions;

eliminated dead code; eliminated redundant bindings; misc tuning;

eliminated dead code;

Sorts.of_sort_derivation: no pp here;

eliminated redundant bindings; schedule_tasks/require_thy: eliminated obsolete tasks_len, which was a leftover from theory-only parallelization;

actually perform Isar_Document.init on startup;

eliminated dead code; eliminated redundant parameters;

removed dead code; Sorts.of_sort_derivation: removed unused pp;

handle Type.TYPE_MATCH, not arbitrary exceptions;

removed redundant Sign.certify_prop, use Sign.cert_prop instead; tuned;

PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;

actually export unit parser;

eliminated dead code;

eliminated redundant parameters;

eliminated redundant bindings;

merged

moved lemmas about sup on bool to Lattices.thy

moved lemmas about sup on bool to Lattices.thy

tuned proofs

tuned headings

report unreferenced ids;

tuned whitespace;

more uniform treatment of structure Unsynchronized in ML bootstrap phase;

merged

mandatory prefix where appropriate

mandatory prefix where appropriate

tuned whitespace

replaced chained_goal by slightly more appropriate flat_goal;

made SML/NJ happy;

added chained_goal, which presents the goal thm as seen by semi-structured methods;

tuned;

removed dead/duplicate code;

aliases for Thomas Sewell;

modernized Balanced_Tree;

replaced meta_iffD2 by existing Drule.equal_elim_rule2; replaced SymSymTab by existing Symreltab; more antiquotations; eliminated old-style Library.foldl, Library.foldl_map; tuned;

tuned header;

Thomas Sewell, NICTA: more efficient HOL/record implementation;

tuned whitespace -- recover basic Isabelle conventions;

merged

Merge with isabelle dev changes.

Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.

Avoid a possible variable name conflict in instantiating a theorem. Instantiating a theorem variable with new variables created a possible variable name conflict if a record was defined with a field named 'f', 'x' etc. Using variable indices of 1 avoids the problem.

Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form.

Merge record patch with updates from isabelle mainline.

Avoid record-inner constants in polymorphic definitions in Bali The Bali package needs to insert a record extension into a type class and define an associated polymorphic constant. There is no elegant way to do this. The existing approach was to insert every record extension into the type class, defining the polymorphic constant at each layer using inner operations created by the record package. Some of those operations have been removed. They can be replaced by use of record_name.extend if necessary, but we can also sidestep this altogether. The simpler approach here is to use defs(overloaded) once to provide a single definition for the composition of all the type constructors, which seems to be permitted. This gets us exactly the fact we need, with the cost that some types that were admitted to the type class have no definition for the constant at all.

Merge with changes from isabelle dev repository.