src/Pure/thm.ML
2012-11-30 ago print formal entities with markup;
2012-11-19 ago theorem status about oracles/futures is no longer printed by default;
2012-08-30 ago proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
2012-07-15 ago prefer canonical fold_rev;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-02-15 ago 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 ago tuned signature;
2012-01-25 ago removed obscure/outdated material;
2012-01-14 ago renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14 ago renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
2011-11-10 ago discontinued unused Thm.compress (again);
2011-11-03 ago tuned signature;
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 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-17 ago more systematic handling of parallel exceptions;
2011-08-09 ago rename_bvs now avoids introducing name clashes between schematic variables
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-08 ago more robust exception pattern General.Subscript;
2011-04-20 ago added Theory.nodes_of convenience;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-02-03 ago thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
2011-02-03 ago tuned comments;
2010-10-28 ago type attribute is derived concept outside the kernel;
2010-10-25 ago recovered some odd two-dimensional layout;
2010-09-24 ago modernized structure Ord_List;
2010-08-25 ago structure Thm: less pervasive names;
2010-06-03 ago eliminated ML structure alias;
2010-06-02 ago always unconstrain thm proofs;
2010-05-19 ago dropped legacy_unconstrainT
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-09 ago reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09 ago Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
2010-05-09 ago just one version of Thm.unconstrainT, which affects all variables;
2010-05-08 ago 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 ago tuned signature;
2010-05-04 ago proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-05-04 ago renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
2010-05-03 ago renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 ago minor tuning of Thm.strip_shyps -- no longer pervasive;
2010-05-03 ago simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
2010-04-25 ago renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
2010-03-27 ago added Term.fold_atyps_sorts convenience;
2010-03-21 ago Logic.mk_of_sort convenience;
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-21 ago explicitly mark some legacy freeze operations;
2009-11-16 ago generalized procs for rewrite_proof: allow skeleton;
2009-11-15 ago tuned;
2009-11-08 ago adapted Theory_Data;
2009-10-25 ago make SML/NJ happy;
2009-10-24 ago maintain explicit name space kind;