20091124 
haftmann 
20091124 
curried take/drop

file  diff  annotate 
20091116 
wenzelm 
20091116 
generalized procs for rewrite_proof: allow skeleton;
fulfill_norm_proof: always normalize result here, no renormalization after filling;

file  diff  annotate 
20091108 
wenzelm 
20091108 
adapted Theory_Data;
tuned;

file  diff  annotate 
20091105 
wenzelm 
20091105 
revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);

file  diff  annotate 
20091104 
wenzelm 
20091104 
fulfill_proof_future: tuned important special case of singleton promise;

file  diff  annotate 
20091029 
wenzelm 
20091029 
standardized filter/filter_out;

file  diff  annotate 
20091021 
haftmann 
20091021 
curried union as canonical list operation

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 parameters;

file  diff  annotate 
20090929 
wenzelm 
20090929 
explicit indication of Unsynchronized.ref;

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 
20090927 
wenzelm 
20090927 
fold_body_thms/join_bodies: explicitly check for cyclic theorem references;

file  diff  annotate 
20090724 
wenzelm 
20090724 
get_name: cover only PThm, not PAxm;

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

file  diff  annotate 
20090719 
wenzelm 
20090719 
tuned;

file  diff  annotate 
20090718 
wenzelm 
20090718 
added join_bodies;

file  diff  annotate 
20090718 
wenzelm 
20090718 
tuned prf_subst: use structure Same;

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 
20090716 
wenzelm 
20090716 
tuned map_proof_terms_option;
eliminated apsome, apsome';
tuned;

file  diff  annotate 
20090716 
wenzelm 
20090716 
use structure Same;
do not open Envir;

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

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

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

file  diff  annotate 
20090325 
wenzelm 
20090325 
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
added approximate_proof_body  replaces former make_proof_body;
added all_oracles_of;
oracle_proof: explicit oracle result;
fulfill_proof/thm_proof: require proper proof_body futures, to maintain full account of oracles and thms (repairs a serious problem of the old version);

file  diff  annotate 
20090324 
wenzelm 
20090324 
status_of: simultaneous list;

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

file  diff  annotate 
20090227 
wenzelm 
20090227 
eliminated NJ's List.nth;

file  diff  annotate 
20090127 
wenzelm 
20090127 
thm_proof: recovered singlethreaded version;

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

file  diff  annotate 
20090127 
wenzelm 
20090127 
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;

file  diff  annotate 
20081231 
wenzelm 
20081231 
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

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 
20081231 
wenzelm 
20081231 
moved old add_term_vars, add_term_frees etc. to structure OldTerm;

file  diff  annotate 
20081230 
wenzelm 
20081230 
freeze_thaw: canonical Term.add_XXX operations;
varify: regular name context;

file  diff  annotate 
20081204 
wenzelm 
20081204 
renamed type Lazy.T to lazy;

file  diff  annotate 
20081123 
wenzelm 
20081123 
tuned;

file  diff  annotate 
20081123 
wenzelm 
20081123 
eliminated finish_proof, keep pre/post normalization of results separate;

file  diff  annotate 
20081118 
wenzelm 
20081118 
fulfill_proof/thm_proof: commuted lazyness;

file  diff  annotate 
20081117 
wenzelm 
20081117 
finish_proof: undefined promises may occur here;

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

file  diff  annotate 
20081116 
wenzelm 
20081116 
proof_body/pthm: removed redundant types field;
fold_proof_atoms: unified recursive case with fold_body_thms;
tuned signature;

file  diff  annotate 
20081116 
berghofe 
20081116 
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.

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

file  diff  annotate 
20080923 
wenzelm 
20080923 
added conditional add_oracles, keep oracles_of_proof private;
added fulfill;
removed unused is_named;
tuned some table operations;

file  diff  annotate 
20080922 
wenzelm 
20080922 
added Promise constructor, which is similar to Oracle but may be replaced later;
added promise_proof;
export min_proof, mk_min_proof;
moved infer_derivs to thm.ML as derive_rule0/1/2;
tuned oracles_of_proof;
added is_named;

file  diff  annotate 
20080623 
wenzelm 
20080623 
Logic.all/mk_equals/mk_implies;

file  diff  annotate 
20080412 
wenzelm 
20080412 
rep_cterm/rep_thm: no longer dereference theory_ref;
removed obsolete compression;

file  diff  annotate 
20080327 
wenzelm 
20080327 
eliminated theory ProtoPure;

file  diff  annotate 
20080319 
haftmann 
20080319 
Type.lookup now curried

file  diff  annotate 
20070711 
berghofe 
20070711 
Added function rew_proof (for prenormalizing proofs).

file  diff  annotate 
20070608 
berghofe 
20070608 
Adapted Proofterm.bicompose_proof to Larry's changes in
Logic.assum_pairs from 20050124 (revision 1.44).

file  diff  annotate 
20070531 
wenzelm 
20070531 
simplified/unified list fold;

file  diff  annotate 
20070507 
wenzelm 
20070507 
simplified DataFun interfaces;

file  diff  annotate 
20070413 
haftmann 
20070413 
canonical merge operations

file  diff  annotate 
20061205 
wenzelm 
20061205 
thm/prf: separate official name vs. additional tags;

file  diff  annotate 
20061004 
haftmann 
20061004 
*** empty log message ***

file  diff  annotate 