src/Pure/thm.ML
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;
2010-04-25 wenzelm 2010-04-25 renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;
2010-03-27 wenzelm 2010-03-27 added Term.fold_atyps_sorts convenience;
2010-03-21 wenzelm 2010-03-21 Logic.mk_of_sort convenience;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
2009-11-16 wenzelm 2009-11-16 generalized procs for rewrite_proof: allow skeleton; fulfill_norm_proof: always normalize result here, no re-normalization after filling;
2009-11-15 wenzelm 2009-11-15 tuned;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;