less ambitious settings;

future_job: more robust Exn.capture outside thread attribute change;

shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;

future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group; control combinators: paranoia eta-expansion to ensure proper operational semantics;

maintain Future.worker_group as management data; cancel_thy: refer to proper task group; tuned;

join_proofs: implicit exception; removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML; tuned;

simultaneous join_proofs; removed obsolete promises_of;

map: subgroup of worker_group;

added worker_group; fork: default to subgroup of worker_group; removed obsolete fork_local; join/get_result: cumulative flattened exceptions; map: subgroup of worker_group;

support for nested groups -- cancellation is propagated to peers and subgroups; added is_canceled; tuned;

added flatten/flatten_list -- supercedes internal plain_exns; represent empty failure as EXCEPTIONS [] instead of Interrupt;

propagate exceptions within future groups; Future.map: inherit group;

less ambitious ML_OPTIONS;

disabled macbroy6 -- hardware repair;

tuned;

tuned tracing; provide spare worker threads to saturate hardware while other workers wait during join;

prefer simultaneous join -- for improved scheduling;

tuned dequeu_towards: try immediate tasks before expensive all_preds;

Display.pretty_thm now requires a proper context;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

moved ProofContext.pretty_thm to Display.pretty_thm etc.; explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; removed some very old thm print operations;

moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;

removed obsolete CVS Ids;

merged

merged

deftab: only process theorems on demand

no SAME exceptions in uncritical code

merged

less digestible

refined outline structure

replaced usedir option -Q by more fine-grained -q;

merged

merged

closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text

merged

merged

simplification of locale interfaces

additional preprocessor rule

added code_unfold_post attribute

more accessors to unfold simpset

clarified code

prefer code_inline over code_unfold; use code_unfold_post where appropriate

tuned code annotations

more canonical import

merged

merged

refinement of lattice classes

removed outdated comment

Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);

parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;

cancel_proofs: some attempts at reworking group management (based on body promises only);

support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies); export promises_of; removed obsolete pending_groups; tuned;

more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);

tuned;

future_result: explicitly impose Variable.sorts_of again;

recovered a version of dequeue_towards (cf. bb7b5a5942c7); join_results: work only towards explicit dependencies -- otherwise could produce dynamic cycle (not recorded in queue);

added join_bodies;

scheduler: tuned tracing (status); join_wait: more robust is_finished check;

added group_id; added status;

synchronized: tuned tracing;

tuned;

tuned prf_subst: use structure Same;

merged

Changed fact_Suc_nat back to fact_Suc

merged

merged

merged

commit merge

Repairs regarding new Fact.thy.

merged

merged

Use term antiquotation to refer to constant names in subsection title.

Repaired uses of factorial.

Automated merge with http://isabelle.in.tum.de/repos/isabelle

Moved factorial lemmas from Binomial.thy to Fact.thy and merged.

tuned/modernized Envir.subst_XXX;

tuned/modernized subst: Same.operation; renamed typ_subst_TVars to subst_type; renamed subst_TVars to subst_term_types; renamed subst_vars to subst_term; removed unused subst_Vars (covered by subst_term);

tuned;

tuned/modernized Envir operations;

major cleanup, simplification, modernization;

eq_type: special case for empty environment;

compare types directly -- no need to invoke Type.eq_type with empty environment;

incr_indexes (from Proofterm);

tuned incr_indexes;

tuned incr_tvar_same; export tuned version of incr_indexes_same;

added same;

tuned map_proof_terms_option; eliminated apsome, apsome'; tuned;

export incr_tvar_same; tuned;

added map_option;

use structure Same;

use structure Same; tuned;

use structure Same; do not open Envir;

use structure Same; tuned signature; tuned comments; tuned;

added map;

use structure Same; more exports; tuned;

Support for copy-avoiding functions on pure values, at the cost of readability.

removed obsolete/unused legacy_varify;

eliminated legacy_varify;

merged

simplified proofs

more antiquotations;

eliminated obsolete legacy_varify;

tuned comment;

Made "prime" executable

More finite set induction rules

made upt/upto executable on nat/int by simp

removed obsolete/unused legacy_unvarify;

tuned prepare_patternT: Term.exists_subtype;

tuned paramify_vars: Term_Subst.map_atypsT_option;

merged

updated to changes in sources; tuned

updated to changes in sources; tuned

code attributes use common underscore convention

NEWS and CONTRIBUTORS

Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.

more gcd/lcm lemmas

typo

resolvd conflict

More about gcd/lcm, and some cleaning up

added boolean_algebra type class; tuned lattice duals