src/Pure/thm.ML
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-07-03 wenzelm 2015-07-03 tuned signature;
2015-05-30 wenzelm 2015-05-30 more explicit context;
2015-04-08 wenzelm 2015-04-08 explicitly checked alpha conversion -- actual renaming happens outside kernel;
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-23 wenzelm 2015-03-23 local fixes may depend on goal params;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature;
2015-03-04 wenzelm 2015-03-04 removed unused; tuned comments;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-11-08 wenzelm 2014-11-08 proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
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;