src/Pure/thm.ML
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-11 wenzelm 2014-03-11 tuned signature;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2013-07-30 wenzelm 2013-07-30 tuned;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-19 wenzelm 2013-07-19 turned pattern unify flag into configuration option (global only);
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-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-29 wenzelm 2013-05-29 unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-04-03 wenzelm 2013-04-03 updated comment to 46b90bbc370d;
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
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;
2012-08-30 wenzelm 2012-08-30 proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
2012-07-15 wenzelm 2012-07-15 prefer canonical fold_rev;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-02-14 wenzelm 2012-02-14 tuned signature;
2012-01-25 wenzelm 2012-01-25 removed obscure/outdated material;
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14 wenzelm 2012-01-14 renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
2011-11-10 wenzelm 2011-11-10 discontinued unused Thm.compress (again);
2011-11-03 wenzelm 2011-11-03 tuned signature;
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 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-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
2011-08-09 berghofe 2011-08-09 rename_bvs now avoids introducing name clashes between schematic variables
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-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-20 wenzelm 2011-04-20 added Theory.nodes_of convenience;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-02-03 wenzelm 2011-02-03 thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
2011-02-03 wenzelm 2011-02-03 tuned comments;
2010-10-28 wenzelm 2010-10-28 type attribute is derived concept outside the kernel;
2010-10-25 wenzelm 2010-10-25 recovered some odd two-dimensional layout;
2010-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
2010-08-25 wenzelm 2010-08-25 structure Thm: less pervasive names;
2010-06-03 wenzelm 2010-06-03 eliminated ML structure alias;
2010-06-02 wenzelm 2010-06-02 always unconstrain thm proofs;
2010-05-19 haftmann 2010-05-19 dropped legacy_unconstrainT
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-09 wenzelm 2010-05-09 reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-08 wenzelm 2010-05-08 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 wenzelm 2010-05-08 tuned signature;
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 renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 minor tuning of Thm.strip_shyps -- no longer pervasive;
2010-05-03 wenzelm 2010-05-03 simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;