src/Pure/proofterm.ML
2016-09-12 wenzelm 2016-09-12 tuned -- fewer warnings;
2016-08-06 wenzelm 2016-08-06 tuned signature;
2016-04-07 wenzelm 2016-04-07 prefer regular context update, to allow continuous editing of Pure;
2016-03-08 haftmann 2016-03-08 provide explicit hint concering uniqueness of derivation
2015-03-23 wenzelm 2015-03-23 local fixes may depend on goal params;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-07-18 wenzelm 2013-07-18 immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
2013-06-27 wenzelm 2013-06-27 manage option "proofs" within theory context -- with minor overhead for primitive inferences;
2013-06-23 wenzelm 2013-06-23 support for XML data representation of proof terms;
2013-04-12 wenzelm 2013-04-12 tuned signature; tuned comments;
2013-02-13 wenzelm 2013-02-13 discontinued home-made sharing for proof terms -- leave memory management to the Poly/ML RTS;
2013-01-24 wenzelm 2013-01-24 avoid extra fork for fulfill_proof_future whenever possible -- without proof terms it merely doubles the number of proof tasks redundantly, by piggy-backing another 10 microseconds task;
2013-01-07 wenzelm 2013-01-07 no fork from draft thy -- avoid potential for crash via classrel_proof/arity_proof;
2012-11-19 wenzelm 2012-11-19 theorem status about oracles/futures is no longer printed by default; renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
2011-10-16 wenzelm 2011-10-16 added Term.dummy_pattern conveniences;
2011-08-20 wenzelm 2011-08-20 more direct balanced version Ord_List.unions;
2011-08-20 wenzelm 2011-08-20 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 wenzelm 2011-08-20 tuned future priorities (again);
2011-08-20 wenzelm 2011-08-20 clarified fulfill_norm_proof: no join_thms yet; clarified priority of fulfill_proof_future, which is followed by explicit join_thms; explicit Thm.future_body_of without join yet; tuned Thm.future_result: join_promises without fulfill_norm_proof;
2011-08-20 wenzelm 2011-08-20 added Future.joins convenience; clarified Future.map: based on Future.cond_forks;
2011-08-19 wenzelm 2011-08-19 incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;
2011-08-19 wenzelm 2011-08-19 tuned;
2011-08-10 wenzelm 2011-08-10 avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10 wenzelm 2011-08-10 avoid OldTerm operations -- with subtle changes of semantics;
2011-08-10 wenzelm 2011-08-10 future_job: explicit indication of interrupts;
2011-08-09 wenzelm 2011-08-09 misc tuning and clarification;
2011-08-09 wenzelm 2011-08-09 tuned whitespace;
2011-07-13 wenzelm 2011-07-13 recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-02-03 wenzelm 2011-02-03 tuned comments;
2011-02-03 wenzelm 2011-02-03 clarified Proofterm.proofs_enabled;
2011-01-31 wenzelm 2011-01-31 tuned signature; tuned vacous forks;
2011-01-31 wenzelm 2011-01-31 support named tasks, for improved tracing;
2011-01-31 wenzelm 2011-01-31 more direct Future.bulk, which potentially reduces overhead for Par_List; tuned signature;
2010-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
2010-09-01 haftmann 2010-09-01 replaced Table.map' by Table.map
2010-06-02 wenzelm 2010-06-02 always unconstrain thm proofs;
2010-06-02 wenzelm 2010-06-02 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 berghofe 2010-06-01 merged
2010-06-01 berghofe 2010-06-01 - outer_constraints with original variable names, to ensure that argsP is consistent with args - Exported map_proof_same, added implies_intr_proof' and forall_intr_proof' - Rewriting procedures used by rewrite_proof can now access hypotheses - Finally enabled unconstrain
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-14 wenzelm 2010-05-14 added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
2010-05-13 wenzelm 2010-05-13 conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
2010-05-13 wenzelm 2010-05-13 avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;
2010-05-13 wenzelm 2010-05-13 raise Fail uniformly for proofterm errors, which appear to be rather low-level;
2010-05-13 wenzelm 2010-05-13 unconstrainT operations on proofs, according to krauss/schropp;
2010-05-13 wenzelm 2010-05-13 added Proofterm.get_name variants according to krauss/schropp; tuned signature;
2010-05-08 wenzelm 2010-05-08 tuned signature;
2010-05-08 wenzelm 2010-05-08 added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
2010-05-08 wenzelm 2010-05-08 back-patching of axclass proofs;
2010-05-07 wenzelm 2010-05-07 strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
2010-05-04 wenzelm 2010-05-04 proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences: * present type variables are only compared wrt. first component (the atomic type), not the duplicated sort; * extra sorts are grounded towards fixed 'a, potentially with different sorts (the original version with Name.names could cause name clashes with other present variables, too, but this should not be a problem); * deriv_rule_unconditional ensures that proof terms are always maintained independently of the "proofs" flag -- this improves robustness and preserves basic PThm proofs required for extraction attributes, e.g. in theory HOL/Extraction;
2010-05-04 wenzelm 2010-05-04 simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-04 wenzelm 2010-05-04 renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);