20091021 
haftmann 
20091021 
curried inter as canonical list operation (beware of argument order)

file  diff  annotate 
20091021 
haftmann 
20091021 
dropped redundant gen_ prefix

file  diff  annotate 
20091020 
haftmann 
20091020 
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

file  diff  annotate 
20091001 
wenzelm 
20091001 
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;

file  diff  annotate 
20090930 
wenzelm 
20090930 
eliminated redundant bindings;

file  diff  annotate 
20090928 
wenzelm 
20090928 
fold_body_thms: pass pthm identifier;
fold_body_thms: dismiss pathetic attempt to check for cycles (cf. e24acd21e60e)  could be masked by "seen";
fulfill_proof/thm_proof: check for thm cycles at the substitution point;

file  diff  annotate 
20090928 
wenzelm 
20090928 
tuned internal source structure;

file  diff  annotate 
20090916 
wenzelm 
20090916 
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;

file  diff  annotate 
20090726 
wenzelm 
20090726 
lambda/cabs/all: named variants;

file  diff  annotate 
20090721 
wenzelm 
20090721 
simultaneous join_proofs;
removed obsolete promises_of;

file  diff  annotate 
20090721 
wenzelm 
20090721 
prefer simultaneous join  for improved scheduling;

file  diff  annotate 
20090719 
wenzelm 
20090719 
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;

file  diff  annotate 
20090717 
wenzelm 
20090717 
tuned/modernized Envir.subst_XXX;

file  diff  annotate 
20090717 
wenzelm 
20090717 
tuned/modernized Envir operations;

file  diff  annotate 
20090716 
wenzelm 
20090716 
tuned incr_indexes;

file  diff  annotate 
20090709 
wenzelm 
20090709 
renamed structure TermSubst to Term_Subst;

file  diff  annotate 
20090706 
wenzelm 
20090706 
clarified strip_shyps: proper type witnesses for present sorts;
moved fold_terms to thm.ML;

file  diff  annotate 
20090706 
wenzelm 
20090706 
structure Thm: less pervasive names;

file  diff  annotate 
20090706 
wenzelm 
20090706 
clarified Thm.of_class/of_sort/class_triv;

file  diff  annotate 
20090706 
wenzelm 
20090706 
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;

file  diff  annotate 
20090702 
wenzelm 
20090702 
strip_shyps: remove top sort, which is logically insignificant;

file  diff  annotate 
20090702 
wenzelm 
20090702 
added proforma proof constructor Inclass;

file  diff  annotate 
20090325 
wenzelm 
20090325 
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
more explicit oracle_proof;

file  diff  annotate 
20090324 
wenzelm 
20090324 
status_of: need to include local promises as well!

file  diff  annotate 
20090324 
wenzelm 
20090324 
display derivation status of thms;

file  diff  annotate 
20090317 
wenzelm 
20090317 
eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
tuned;

file  diff  annotate 
20090316 
wenzelm 
20090316 
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);

file  diff  annotate 
20090312 
wenzelm 
20090312 
renamed NameSpace.bind to NameSpace.define;

file  diff  annotate 
20090307 
wenzelm 
20090307 
moved Thm.def_name(_optional) to more_thm.ML;
moved oldstyle Thm.get_def to Drule.get_def;

file  diff  annotate 
20090305 
wenzelm 
20090305 
Thm.add_oracle interface: replaced old bstring by binding;

file  diff  annotate 
20090127 
wenzelm 
20090127 
thm_proof: replaced lazy by composed futures;

file  diff  annotate 
20090110 
wenzelm 
20090110 
future_result: avoid expensive norm_proof (consider usedir option Q false in lowmemory situations);

file  diff  annotate 
20090110 
wenzelm 
20090110 
added pending_groups  accumulates task groups of local derivations only;

file  diff  annotate 
20090101 
wenzelm 
20090101 
avoid polymorphic equality;

file  diff  annotate 
20081231 
wenzelm 
20081231 
use regular Term.add_XXX etc.;

file  diff  annotate 
20081231 
wenzelm 
20081231 
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

file  diff  annotate 
20081206 
wenzelm 
20081206 
renamed force_proof to join_proof;

file  diff  annotate 
20081205 
wenzelm 
20081205 
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
name_thm: actually maintain max_promise/open_promises here (!), reduce open_promises as far as possible;
tuned;

file  diff  annotate 
20081205 
haftmann 
20081205 
merged

file  diff  annotate 
20081205 
haftmann 
20081205 
dropped NameSpace.declare_base

file  diff  annotate 
20081205 
wenzelm 
20081205 
merged

file  diff  annotate 
20081204 
wenzelm 
20081204 
future proofs: pass actual futures to facilitate composite computations;
removed join_futures  superceded by higherlevel PureThy.force_proofs;

file  diff  annotate 
20081204 
haftmann 
20081204 
cleaned up binding module and related code

file  diff  annotate 
20081123 
wenzelm 
20081123 
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);

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

file  diff  annotate 
20081118 
wenzelm 
20081118 
added force_proofs;
join_futures: no errors here;

file  diff  annotate 
20081117 
wenzelm 
20081117 
tuned promise/fullfill;

file  diff  annotate 
20081116 
wenzelm 
20081116 
put_name/thm_proof: promises are filled with fulfilled proofs;
tuned;

file  diff  annotate 
20081116 
wenzelm 
20081116 
clarified Thm.proof_body_of vs. Thm.proof_of;

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

file  diff  annotate 
20081023 
wenzelm 
20081023 
renamed get_axiom_i to axiom, removed obsolete get_axiom;
reduced pervasive names;

file  diff  annotate 
20081021 
wenzelm 
20081021 
join results in isolation;

file  diff  annotate 
20081016 
wenzelm 
20081016 
added weaken_sorts;
strip_shyps: minimal list of minimized extra sorts;
tuned;

file  diff  annotate 
20081001 
wenzelm 
20081001 
renamed promise to future, tuned related interfaces;

file  diff  annotate 
20081001 
wenzelm 
20081001 
more precise join_futures, improved termination;

file  diff  annotate 
20080930 
wenzelm 
20080930 
export explicit joint_futures, removed Theory.at_end hook;
renamed Future.fork_irrelevant to Future.fork_background;

file  diff  annotate 
20080928 
wenzelm 
20080928 
join earlier promises first;

file  diff  annotate 
20080928 
wenzelm 
20080928 
promise_result: enforce strictly sequential dependencies, via serial numbers;

file  diff  annotate 
20080927 
wenzelm 
20080927 
Future.release_results;

file  diff  annotate 
20080927 
wenzelm 
20080927 
promise: include check into future body, i.e. joined results are always valid;
pending future derivations: shared ref within whole theory body, i.e. endoftheory joins *all* derivations ever forked from a version of the theory;
simplified rep_deriv;

file  diff  annotate 