src/Pure/proofterm.ML
2012-11-19 ago theorem status about oracles/futures is no longer printed by default;
2011-10-16 ago added Term.dummy_pattern conveniences;
2011-08-20 ago more direct balanced version Ord_List.unions;
2011-08-20 ago reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
2011-08-20 ago tuned future priorities (again);
2011-08-20 ago clarified fulfill_norm_proof: no join_thms yet;
2011-08-20 ago added Future.joins convenience;
2011-08-19 ago incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
2011-08-19 ago tuned;
2011-08-10 ago avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10 ago avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10 ago future_job: explicit indication of interrupts;
2011-08-09 ago misc tuning and clarification;
2011-08-09 ago tuned whitespace;
2011-07-13 ago recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
2011-07-11 ago tuned signature -- corresponding to Scala version;
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-06-09 ago simplified Name.variant -- discontinued builtin fold_map;
2011-06-09 ago discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-08 ago more robust exception pattern General.Subscript;
2011-02-03 ago tuned comments;
2011-02-03 ago clarified Proofterm.proofs_enabled;
2011-01-31 ago tuned signature;
2011-01-31 ago support named tasks, for improved tracing;
2011-01-31 ago more direct Future.bulk, which potentially reduces overhead for Par_List;
2010-09-24 ago modernized structure Ord_List;
2010-09-01 ago replaced Table.map' by Table.map
2010-06-02 ago always unconstrain thm proofs;
2010-06-02 ago normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
2010-06-01 ago merged
2010-06-01 ago - outer_constraints with original variable names, to ensure that argsP is consistent with args
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
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-13 ago avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
2010-05-13 ago raise Fail uniformly for proofterm errors, which appear to be rather low-level;
2010-05-13 ago unconstrainT operations on proofs, according to krauss/schropp;
2010-05-13 ago added Proofterm.get_name variants according to krauss/schropp;
2010-05-08 ago tuned signature;
2010-05-08 ago added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08 ago back-patching of axclass proofs;
2010-05-07 ago strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-04 ago proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-05-04 ago simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-04 ago renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-03-21 ago do not open ML structures;
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-16 ago generalized procs for rewrite_proof: allow skeleton;
2009-11-08 ago adapted Theory_Data;
2009-11-05 ago revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);
2009-11-04 ago fulfill_proof_future: tuned important special case of singleton promise;
2009-10-29 ago standardized filter/filter_out;
2009-10-21 ago curried union as canonical list operation
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 parameters;