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

move Kleene_Algebra to Library

merged

tuned locale interface

tuned

dropped find_index_eq

tuned quickcheck generator for bool

tuned

merged

merged

tuned varify/unvarify: use Term_Subst.map_XXX combinators;

added some generic mapping combinators; share private exception SAME locally;

reorganised; many new lemmas thanks to sledgehammer

tuned

renamed structure TermSubst to Term_Subst;

Sorttab in Pure;

removed obsolete CVS Ids;

removed obsolete CVS Ids;

merged

recovered some proofs broken in 0314441a53a6;

renamed functor TableFun to Table, and GraphFun to Graph;

move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure

drop unused lemmas

FPS form a metric space, which justifies the infinte sum notation

merged

merged

merged

merged

Gettring rid of sorts hyps

tuned structure Code internally

merged

name fixed

merged

merged

tuned interface of structure Code

more accurate certificates for constant aliasses

merged

Stefan Berghofer's code generator uses Pure equality instead of HOL equality now

fixed proof (cf. 40501bb2d57c);

renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int

merged

tuned code

moved Inductive.myinv to Fun.inv; tuned

add_classrel/arity: strip_shyps of stored result;

clarified strip_shyps: proper type witnesses for present sorts; moved fold_terms to thm.ML;

witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;

structure Thm: less pervasive names;

clarified Thm.of_class/of_sort/class_triv;