2010-05-19 ago dropped legacy_unconstrainT
2010-05-14 ago added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
2010-05-13 ago conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
2010-05-09 ago reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09 ago Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09 ago just one version of Thm.unconstrainT, which affects all variables;
2010-05-08 ago renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-05-08 ago tuned signature;
2010-05-04 ago proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-05-04 ago renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-05-03 ago renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 ago minor tuning of Thm.strip_shyps -- no longer pervasive;
2010-05-03 ago simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
2010-04-25 ago renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-03-27 ago added Term.fold_atyps_sorts convenience;
2010-03-21 ago Logic.mk_of_sort convenience;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-27 ago modernized structure Term_Ord;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-21 ago explicitly mark some legacy freeze operations;
2009-11-16 ago generalized procs for rewrite_proof: allow skeleton;
2009-11-15 ago tuned;
2009-11-08 ago adapted Theory_Data;
2009-10-25 ago make SML/NJ happy;
2009-10-24 ago maintain explicit name space kind;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-10-21 ago curried inter as canonical list operation (beware of argument order)
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-01 ago 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;
2009-09-30 ago eliminated redundant bindings;
2009-09-28 ago fold_body_thms: pass pthm identifier;
2009-09-28 ago tuned internal source structure;
2009-09-16 ago replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
2009-07-26 ago lambda/cabs/all: named variants;
2009-07-21 ago simultaneous join_proofs;
2009-07-21 ago prefer simultaneous join -- for improved scheduling;
2009-07-19 ago support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
2009-07-17 ago tuned/modernized Envir.subst_XXX;
2009-07-17 ago tuned/modernized Envir operations;
2009-07-16 ago tuned incr_indexes;
2009-07-09 ago renamed structure TermSubst to Term_Subst;
2009-07-06 ago clarified strip_shyps: proper type witnesses for present sorts;
2009-07-06 ago structure Thm: less pervasive names;
2009-07-06 ago clarified Thm.of_class/of_sort/class_triv;
2009-07-06 ago renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 ago strip_shyps: remove top sort, which is logically insignificant;
2009-07-02 ago added pro-forma proof constructor Inclass;
2009-03-25 ago fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
2009-03-24 ago status_of: need to include local promises as well!
2009-03-24 ago display derivation status of thms;
2009-03-17 ago eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
2009-03-16 ago substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
2009-03-12 ago renamed NameSpace.bind to NameSpace.define;
2009-03-07 ago moved Thm.def_name(_optional) to more_thm.ML;
2009-03-05 ago Thm.add_oracle interface: replaced old bstring by binding;
2009-01-27 ago thm_proof: replaced lazy by composed futures;
2009-01-10 ago future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);