src/Pure/thm.ML
2017-06-22 wenzelm 2017-06-22 consolidate proofs more simultaneously;
2017-04-10 wenzelm 2017-04-10 tuned signature;
2017-02-03 wenzelm 2017-02-03 proper background certificate from make_context, which can be a super-theory of the direct join (amending d07464875dd4);
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;
2016-12-15 wenzelm 2016-12-15 back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
2016-12-14 wenzelm 2016-12-14 more careful derivation_closed / close_derivation;
2016-09-12 wenzelm 2016-09-12 tuned;
2016-08-05 wenzelm 2016-08-05 tuned whitespace;
2015-08-30 wenzelm 2015-08-30 tuned;
2015-08-30 wenzelm 2015-08-30 clarified exceptions; tuned signature;
2015-08-30 wenzelm 2015-08-30 clarified exceptions; more careful treatment of missing context;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-08-30 wenzelm 2015-08-30 clarified exceptions;
2015-08-28 wenzelm 2015-08-28 clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in user-space);
2015-08-28 wenzelm 2015-08-28 more abstract theory certificate, which is not necessarily the full theory;
2015-08-28 wenzelm 2015-08-28 tuned signature;
2015-08-28 wenzelm 2015-08-28 tuned signature;
2015-08-16 wenzelm 2015-08-16 produce certified vars without access to theory_of_thm, and without context;
2015-08-16 wenzelm 2015-08-16 produce certified vars without access to theory_of_thm, and without context;
2015-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-08-16 wenzelm 2015-08-16 prefer theory_id operations; tuned signature;
2015-08-15 wenzelm 2015-08-15 obsolete;
2015-07-28 wenzelm 2015-07-28 more direct access to atomic cterms;
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;