src/Pure/proofterm.ML
9 months ago wenzelm 2019-08-14 clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);
9 months ago wenzelm 2019-08-14 tuned;
9 months ago wenzelm 2019-08-14 uniform standard_vars for terms and proof terms;
9 months ago wenzelm 2019-08-12 tuned -- eliminated unused parameters;
9 months ago wenzelm 2019-08-12 more direct/compact export of proof terms;
9 months ago wenzelm 2019-08-10 more careful export of unnamed proof boxes: avoid duplicates via memoing;
9 months ago wenzelm 2019-08-10 tuned signature;
9 months ago wenzelm 2019-08-10 export each PThm node separately: slightly more scalable;
9 months ago wenzelm 2019-08-10 more positions;
9 months ago wenzelm 2019-08-09 tuned;
9 months ago wenzelm 2019-08-09 formal position for PThm nodes;
9 months ago wenzelm 2019-08-09 clarified ML types;
9 months ago wenzelm 2019-08-09 proper treatment of body oracles, outside of recursion into thms graph;
10 months ago wenzelm 2019-08-02 more direct proofs for type classes; misc tuning and cleanup;
10 months ago wenzelm 2019-08-01 clarified module structure;
10 months ago wenzelm 2019-07-31 clarified export: retain proof boxes as local definitions -- more scalable;
10 months ago wenzelm 2019-07-30 clarified global theory context;
10 months ago wenzelm 2019-07-30 more robust export, based on reconstruct_proof / expand_proof;
10 months ago wenzelm 2019-07-30 clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
10 months ago wenzelm 2019-07-30 discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;
10 months ago wenzelm 2019-07-29 more diagnostic operations;
10 months ago wenzelm 2019-07-29 tuned -- non-strict args;
10 months ago wenzelm 2019-07-29 tuned signature;
10 months ago wenzelm 2019-07-29 clarified signature; tuned;
10 months ago wenzelm 2019-07-29 tuned signature;
10 months ago wenzelm 2019-07-27 tuned;
10 months ago wenzelm 2019-07-27 tuned;
10 months ago wenzelm 2019-07-26 tuned -- reorder sections;
10 months ago wenzelm 2019-07-26 tuned;
10 months ago wenzelm 2019-07-26 tuned signature;
10 months ago wenzelm 2019-07-26 tuned;
10 months ago wenzelm 2019-07-26 finalize proofs earlier to reduce memory requirement;
10 months ago wenzelm 2019-07-26 more explicit type proof_serial;
10 months ago wenzelm 2019-07-26 defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement; misc tuning and clarification;
10 months ago wenzelm 2019-07-24 prefer local counter;
10 months ago wenzelm 2019-07-24 more accurate proof export;
10 months ago wenzelm 2019-07-24 tuned;
10 months ago wenzelm 2019-07-24 more thorough clean_proof;
10 months ago wenzelm 2019-07-23 treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
10 months ago wenzelm 2019-07-23 clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named; added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;
10 months ago wenzelm 2019-07-23 tuned comments;
10 months ago wenzelm 2019-07-23 proof terms are always constructed sequentially; discontinued unused Proofterm.Promise -- too complex;
10 months ago wenzelm 2019-07-22 tuned comments -- proper sections;
10 months ago wenzelm 2019-07-22 support export_proofs, prune_proofs; tuned comments;
10 months ago wenzelm 2019-07-22 clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
10 months ago wenzelm 2019-07-22 tuned;
10 months ago wenzelm 2019-07-22 clarified exception;
10 months ago wenzelm 2019-07-22 tuned;
10 months ago wenzelm 2019-07-22 more accurate type information;
10 months ago wenzelm 2019-07-21 global declaration of abstract syntax for proof terms, with qualified names; clarified modules;
2018-05-02 wenzelm 2018-05-02 tuned -- slightly smaller future closure size;
2018-04-24 wenzelm 2018-04-24 more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;
2018-04-24 wenzelm 2018-04-24 less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);
2018-02-19 wenzelm 2018-02-19 tuned: more parallel;
2017-06-22 wenzelm 2017-06-22 consolidate proofs more simultaneously;
2017-06-22 wenzelm 2017-06-22 more informative task_statistics;
2017-04-09 wenzelm 2017-04-09 tuned signature -- prefer qualified names;
2016-12-16 wenzelm 2016-12-16 consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d;
2016-12-16 wenzelm 2016-12-16 tuned signature -- more abstract type thm_node;
2016-12-15 wenzelm 2016-12-15 tuned signature;